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 /interp/constrextern.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 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 2e74b809f4..d45e6b9b37 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -28,6 +28,8 @@ open Nametab open Notation open Reserve open Detyping +open Misctypes +open Decl_kinds (*i*) (* Translation from glob_constr to front constr *) @@ -218,7 +220,7 @@ let rec check_same_type ty1 ty2 = | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () | CSort(_,s1), CSort(_,s2) when s1=s2 -> () - | CCast(_,a1,CastConv (_,b1)), CCast(_,a2, CastConv(_,b2)) -> + | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) -> check_same_type a1 a2; check_same_type b1 b2 | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) -> @@ -644,7 +646,8 @@ let extern_optimal_prim_token scopes r r' = (* mapping glob_constr to constr_expr *) let extern_glob_sort = function - | GProp _ as s -> s + | GProp -> GProp + | GSet -> GSet | GType (Some _) as s when !print_universes -> s | GType _ -> GType None @@ -811,10 +814,9 @@ let rec extern inctx scopes vars r = | GHole (loc,e) -> CHole (loc, Some e) - | GCast (loc,c, CastConv (k,t)) -> - CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t)) - | GCast (loc,c, CastCoerce) -> - CCast (loc,sub_extern true scopes vars c, CastCoerce) + | GCast (loc,c, c') -> + CCast (loc,sub_extern true scopes vars c, + Miscops.map_cast_type (extern_typ scopes vars) c') and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes) |