Mentions légales du service

Skip to content
Snippets Groups Projects

Adapt w.r.t. coq/coq#16933.

Merged Adapt w.r.t. coq/coq#16933.
pedrot/itauto:esorts-respect-api into master
Merged Pierre-Marie Pédrot requested to merge pedrot/itauto:esorts-respect-api into master
Compare
and
2 files
+ 2
− 2
Compare changes
  • Side-by-side
  • Inline
Files
2
src/cdcl.ml
+ 1
− 1
@@ -119,7 +119,7 @@ let get_projection env evd c =
let is_prop env sigma term =
let sort = Retyping.get_sort_of env sigma term in
Sorts.is_prop sort
Sorts.is_prop (EConstr.ESorts.kind sigma sort)
let constr_of_option typ constr_of_val = function
| None -> EConstr.mkApp (Lazy.force coq_None, [|typ|])