From 5fa47f1258408541150e2e4c26d60ff694e7c1bc Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:37 +0000
Subject: 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
---
 interp/constrextern.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'interp/constrextern.ml')

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)
-- 
cgit v1.2.3