diff options
| author | letouzey | 2012-05-29 11:08:37 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:37 +0000 |
| commit | 5fa47f1258408541150e2e4c26d60ff694e7c1bc (patch) | |
| tree | 9e7aee1ea714cebdccc50dbd85735948d8baeaf0 /pretyping/unification.ml | |
| parent | 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 (diff) | |
locus.mli for occurrences+clauses, misctypes.mli for various little things
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 2344f6e46e..fd40cca7c1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -25,6 +25,7 @@ open Pretype_errors open Retyping open Coercion open Recordops +open Locus let occur_meta_or_undefined_evar evd c = let rec occrec c = match kind_of_term c with @@ -56,7 +57,7 @@ let abstract_scheme env c l lname_typ = let abstract_list_all env evd typ c l = let ctxt,_ = splay_prod_n env evd (List.length l) typ in - let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in + let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in let p = abstract_scheme env c l_with_all_occs ctxt in try if is_conv_leq env evd (Typing.type_of env evd p) typ then p @@ -65,7 +66,7 @@ let abstract_list_all env evd typ c l = error_cannot_find_well_typed_abstraction env evd p l let set_occurrences_of_last_arg args = - Some all_occurrences :: List.tl (array_map_to_list (fun _ -> None) args) + Some AllOccurrences :: List.tl (array_map_to_list (fun _ -> None) args) let abstract_list_all_with_dependencies env evd typ c l = let evd,ev = new_evar evd env typ in |