diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 14 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 6 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 198 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 3 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 19 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/program.ml | 20 | ||||
| -rw-r--r-- | pretyping/program.mli | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 16 |
10 files changed, 149 insertions, 138 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4261573725..80680e4088 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -731,7 +731,7 @@ let get_names env sigma sign eqns = (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in - (na::l,(out_name na)::avoid)) + (na::l,(Name.get_id na)::avoid)) ([],allvars) (List.rev sign) names2 in names3,aliasname @@ -2223,14 +2223,14 @@ let build_ineqs evdref prevpatterns pats liftsign = (Some ([], 0, 0, [])) eqnpats pats in match acc with None -> c - | Some (sign, len, _, c') -> - let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c')) - (lift_rel_context liftsign sign) - in - conj :: c) + | Some (sign, len, _, c') -> + let sigma, conj = mk_coq_and !evdref c' in + let sigma, neg = mk_coq_not sigma conj in + let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in + evdref := sigma; conj :: c) [] prevpatterns in match diffs with [] -> None - | _ -> Some (mk_coq_and diffs) + | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj) let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let i = ref 0 in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 752819aa39..6f099c8dfd 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -907,8 +907,7 @@ let simple_cases_matrix_of_branches ind brs = let nal,c = it_destRLambda_or_LetIn_names n b in let mkPatVar na = CAst.make @@ PatVar na in let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in - let map name = try Some (Nameops.out_name name) with Failure _ -> None in - let ids = List.map_filter map nal in + let ids = List.map_filter Nameops.Name.to_option nal in Loc.tag @@ (ids,[p],c)) brs diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bf62cea6b6..630f80ad2f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -638,7 +638,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = @@ -755,7 +755,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 @@ -816,7 +816,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max n1 n2 in + let na = Nameops.Name.pick n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 923d7d9388..e53d19b595 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -12,6 +12,7 @@ open Nameops open Globnames open Misctypes open Glob_term +open Evar_kinds (* Untyped intermediate terms, after ASTs and before constr. *) @@ -33,109 +34,108 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = (na,k,comp1,comp2) let binding_kind_eq bk1 bk2 = match bk1, bk2 with -| Decl_kinds.Explicit, Decl_kinds.Explicit -> true -| Decl_kinds.Implicit, Decl_kinds.Implicit -> true -| _ -> false + | Decl_kinds.Explicit, Decl_kinds.Explicit -> true + | Decl_kinds.Implicit, Decl_kinds.Implicit -> true + | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false let case_style_eq s1 s2 = match s1, s2 with -| LetStyle, LetStyle -> true -| IfStyle, IfStyle -> true -| LetPatternStyle, LetPatternStyle -> true -| MatchStyle, MatchStyle -> true -| RegularStyle, RegularStyle -> true -| _ -> false + | LetStyle, LetStyle -> true + | IfStyle, IfStyle -> true + | LetPatternStyle, LetPatternStyle -> true + | MatchStyle, MatchStyle -> true + | RegularStyle, RegularStyle -> true + | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with -| PatVar na1, PatVar na2 -> Name.equal na1 na2 -| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> - eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && - Name.equal na1 na2 -| _ -> false + | PatVar na1, PatVar na2 -> Name.equal na1 na2 + | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> + eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Name.equal na1 na2 + | (PatVar _ | PatCstr _), _ -> false let cast_type_eq eq t1 t2 = match t1, t2 with -| CastConv t1, CastConv t2 -> eq t1 t2 -| CastVM t1, CastVM t2 -> eq t1 t2 -| CastCoerce, CastCoerce -> true -| CastNative t1, CastNative t2 -> eq t1 t2 -| _ -> false - -let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with -| GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 -| GVar id1, GVar id2 -> Id.equal id1 id2 -| GEvar (id1, arg1), GEvar (id2, arg2) -> - Id.equal id1 id2 && - List.equal instance_eq arg1 arg2 -| GPatVar (b1, pat1), GPatVar (b2, pat2) -> - (b1 : bool) == b2 && Id.equal pat1 pat2 -| GApp (f1, arg1), GApp (f2, arg2) -> - glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2 -| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> - Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> - case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && - List.equal tomatch_tuple_eq tp1 tp2 && - List.equal cases_clause_eq cl1 cl2 -| GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> - List.equal Name.equal na1 na2 && Name.equal n1 n2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> - glob_constr_eq m1 m2 && Name.equal pat1 pat2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> - fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && - Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 && - Array.equal glob_constr_eq c1 c2 && - Array.equal glob_constr_eq t1 t2 -| GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 -| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) && - Miscops.intro_pattern_naming_eq nam1 nam2 -| GCast (c1, t1), GCast (c2, t2) -> - glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 -| _ -> false - -and tomatch_tuple_eq (c1, p1) (c2, p2) = + | CastConv t1, CastConv t2 -> eq t1 t2 + | CastVM t1, CastVM t2 -> eq t1 t2 + | CastCoerce, CastCoerce -> true + | CastNative t1, CastNative t2 -> eq t1 t2 + | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + +let matching_var_kind_eq k1 k2 = match k1, k2 with +| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 +| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2 +| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false + +let tomatch_tuple_eq f (c1, p1) (c2, p2) = let eqp (_, (i1, na1)) (_, (i2, na2)) = eq_ind i1 i2 && List.equal Name.equal na1 na2 in let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in - glob_constr_eq c1 c2 && eq_pred p1 p2 + f c1 c2 && eq_pred p1 p2 -and cases_clause_eq (_, (id1, p1, c1)) (_, (id2, p2, c2)) = - List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && - glob_constr_eq c1 c2 +and cases_clause_eq f (_, (id1, p1, c1)) (_, (id2, p2, c2)) = + List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && f c1 c2 -and glob_decl_eq (na1, bk1, c1, t1) (na2, bk2, c2, t2) = +let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - Option.equal glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 - -and fix_kind_eq k1 k2 = match k1, k2 with -| GFix (a1, i1), GFix (a2, i2) -> - let eq (i1, o1) (i2, o2) = - Option.equal Int.equal i1 i2 && fix_recursion_order_eq o1 o2 - in - Int.equal i1 i2 && Array.equal eq a1 a1 -| GCoFix i1, GCoFix i2 -> Int.equal i1 i2 -| _ -> false - -and fix_recursion_order_eq o1 o2 = match o1, o2 with -| GStructRec, GStructRec -> true -| GWfRec c1, GWfRec c2 -> glob_constr_eq c1 c2 -| GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> - glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2 -| _ -> false - -and instance_eq (x1,c1) (x2,c2) = - Id.equal x1 x2 && glob_constr_eq c1 c2 + Option.equal f c1 c2 && f t1 t2 + +let fix_recursion_order_eq f o1 o2 = match o1, o2 with + | GStructRec, GStructRec -> true + | GWfRec c1, GWfRec c2 -> f c1 c2 + | GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> + f c1 c2 && Option.equal f o1 o2 + | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false + +let fix_kind_eq f k1 k2 = match k1, k2 with + | GFix (a1, i1), GFix (a2, i2) -> + let eq (i1, o1) (i2, o2) = + Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 + in + Int.equal i1 i2 && Array.equal eq a1 a1 + | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 + | (GFix _ | GCoFix _), _ -> false + +let instance_eq f (x1,c1) (x2,c2) = + Id.equal x1 x2 && f c1 c2 + +let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with + | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 + | GVar id1, GVar id2 -> Id.equal id1 id2 + | GEvar (id1, arg1), GEvar (id2, arg2) -> + Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 + | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2 + | GApp (f1, arg1), GApp (f2, arg2) -> + f f1 f2 && List.equal f arg1 arg2 + | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> + Name.equal na1 na2 && f b1 b2 && Option.equal f t1 t2 && f c1 c2 + | GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> + case_style_eq st1 st2 && Option.equal f c1 c2 && + List.equal (tomatch_tuple_eq f) tp1 tp2 && + List.equal (cases_clause_eq f) cl1 cl2 + | GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> + List.equal Name.equal na1 na2 && Name.equal n1 n2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> + f m1 m2 && Name.equal pat1 pat2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && + Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && + Array.equal f c1 c2 && Array.equal f t1 t2 + | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 + | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> + Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Miscops.intro_pattern_naming_eq nam1 nam2 + | GCast (c1, t1), GCast (c2, t2) -> + f c1 c2 && cast_type_eq f t1 t2 + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + +let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c let map_glob_constr_left_to_right f = CAst.map (function | GApp (g,args) -> @@ -215,20 +215,20 @@ let fold_glob_constr f acc = CAst.with_val (function ) let fold_return_type_with_binders f g v acc (na,tyopt) = - Option.fold_left (f (name_fold g na v)) acc tyopt + Option.fold_left (f (Name.fold_right g na v)) acc tyopt let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left (f v) (f v acc c) args | GLambda (na,_,b,c) | GProd (na,_,b,c) -> - f (name_fold g na v) (f v acc b) c + f (Name.fold_right g na v) (f v acc b) c | GLetIn (na,b,t,c) -> - f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c + f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c | GCases (_,rtntypopt,tml,pl) -> let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in let fold_tomatch (v',acc) (tm,(na,onal)) = - (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (name_fold g) nal v'') - (name_fold g na v') onal, + (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'') + (Name.fold_right g na v') onal, f v acc tm) in let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in let acc = Option.fold_left (f v') acc rtntypopt in @@ -242,7 +242,7 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function let v,acc = List.fold_left (fun (v,acc) (na,k,bbd,bty) -> - (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty)) + (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty)) (v,acc) bll.(i) in f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in @@ -371,12 +371,12 @@ let loc_of_glob_constr c = c.CAst.loc let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l let test_id l id = if collide_id l id then raise Not_found -let test_na l na = name_iter (test_id l) na +let test_na l na = Name.iter (test_id l) na let update_subst na l = let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in - let l' = name_fold Id.List.remove_assoc na l in - name_fold + let l' = Name.fold_right Id.List.remove_assoc na l in + Name.fold_right (fun id _ -> if in_range id l' then let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index aa48516aff..f7cc08ca21 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -36,6 +36,9 @@ val map_glob_constr_left_to_right : val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit +val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) -> + glob_constr -> glob_constr -> bool + val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 1c8ad0cddd..71dbc39f3f 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -143,7 +143,7 @@ let pattern_of_constr env sigma t = match kind_of_term f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> Some id + Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id | _ -> None) | _ -> None with @@ -156,13 +156,14 @@ let pattern_of_constr env sigma t = pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - assert (not b); PMeta (Some id) + | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) -> + PMeta (Some id) | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) else PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) | Case (ci,p,a,br) -> @@ -329,26 +330,26 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) - | GPatVar (false,n) -> + | GPatVar (Evar_kinds.FirstOrderPatVar n) -> metas := n::!metas; PMeta (Some n) | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ({ CAst.v = GPatVar (true,n) }, cl) -> + | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) | GLambda (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GProd (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GLetIn (na,c1,t,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) @@ -411,7 +412,7 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function | { CAst.v = PatVar na } -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; na | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b0663af70c..1839c87b1c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -625,13 +625,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GPatVar (someta,n) -> + | GPatVar kind -> let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - let k = Evar_kinds.MatchingVar (someta,n) in + let k = Evar_kinds.MatchingVar kind in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> diff --git a/pretyping/program.ml b/pretyping/program.ml index 8769c5659e..2fa3facb30 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -9,7 +9,6 @@ open CErrors open Util -let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = @@ -39,20 +38,25 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" -let coq_not = init_constant ["Init";"Logic"] "not" -let coq_and = init_constant ["Init";"Logic"] "and" +let coq_not = init_reference ["Init";"Logic"] "not" +let coq_and = init_reference ["Init";"Logic"] "and" -let delayed_force c = EConstr.of_constr (c ()) +let new_global sigma gr = + let open Sigma in + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c -let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |]) +let mk_coq_not sigma x = + let sigma, notc = new_global sigma (coq_not ()) in + sigma, EConstr.mkApp (notc, [| x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> invalid_arg "unsafe_fold_right" -let mk_coq_and l = - let and_typ = delayed_force coq_and in - unsafe_fold_right +let mk_coq_and sigma l = + let sigma, and_typ = new_global sigma (coq_and ()) in + sigma, unsafe_fold_right (fun c conj -> EConstr.mkApp (and_typ, [| c ; conj |])) l diff --git a/pretyping/program.mli b/pretyping/program.mli index 94a7bdcb6d..8439b9528c 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference val coq_JMeq_ind : unit -> global_reference val coq_JMeq_refl : unit -> global_reference -val mk_coq_and : constr list -> constr -val mk_coq_not : constr -> constr +val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr +val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e7c9635829..5a2328aaa4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1317,19 +1317,23 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) + let open Universes in let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in try - let fold cstr sigma = - try Some (Evd.add_universe_constraints sigma cstr) - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None - in + let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + in + let ans = match ans with + | None -> None + | Some cstr -> + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with | None -> false, sigma |