aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml25
-rw-r--r--vernac/auto_ind_decl.ml176
-rw-r--r--vernac/class.ml27
-rw-r--r--vernac/classes.ml29
-rw-r--r--vernac/command.ml122
-rw-r--r--vernac/command.mli2
-rw-r--r--vernac/discharge.ml2
-rw-r--r--vernac/explainErr.ml1
-rw-r--r--vernac/himsg.ml257
-rw-r--r--vernac/himsg.mli3
-rw-r--r--vernac/indschemes.ml9
-rw-r--r--vernac/lemmas.ml15
-rw-r--r--vernac/lemmas.mli6
-rw-r--r--vernac/obligations.ml19
-rw-r--r--vernac/record.ml24
-rw-r--r--vernac/search.ml34
-rw-r--r--vernac/vernacentries.ml30
17 files changed, 464 insertions, 317 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 8865cd646..deb2ed3e0 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -144,6 +144,27 @@ let label_of = function
| ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
| VarRef id -> Label.of_id id
+let fold_constr_with_full_binders g f n acc c =
+ let open Context.Rel.Declaration in
+ match kind_of_term c with
+ | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (p,c) -> f n acc c
+ | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
let rec traverse current ctx accu t = match kind_of_term t with
| Var id ->
let body () = id |> Global.lookup_named |> NamedDecl.get_value in
@@ -166,10 +187,10 @@ let rec traverse current ctx accu t = match kind_of_term t with
traverse_object
~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
| _ ->
- Termops.fold_constr_with_full_binders
+ fold_constr_with_full_binders
Context.Rel.add (traverse current) ctx accu t
end
-| _ -> Termops.fold_constr_with_full_binders
+| _ -> fold_constr_with_full_binders
Context.Rel.add (traverse current) ctx accu t
and traverse_object ?inhabits (curr, data, ax2ty) body obj =
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 6d71601cc..b9c4c6cc5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -105,7 +105,7 @@ let mkFullInd (ind,u) n =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
if nparrec > 0
then mkApp (mkIndU (ind,u),
- Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec))
+ Array.of_list(Context.Rel.to_extended_list mkRel (nparrec+n) lnamesparrec))
else mkIndU (ind,u)
let check_bool_is_defined () =
@@ -140,7 +140,7 @@ let build_beq_scheme mode kn =
| Name s -> Id.of_string ("eq_"^(Id.to_string s))
| Anonymous -> Id.of_string "eq_A"
in
- let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in
+ let ext_rel_list = Context.Rel.to_extended_list mkRel 0 lnamesparrec in
let lift_cnt = ref 0 in
let eqs_typ = List.map (fun aa ->
let a = lift !lift_cnt aa in
@@ -179,9 +179,10 @@ let build_beq_scheme mode kn =
*)
let compute_A_equality rel_list nlist eqA ndx t =
let lifti = ndx in
+ let sigma = Evd.empty (** FIXME *) in
let rec aux c =
let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
| Var x ->
let eid = id_of_string ("eq_"^(string_of_id x)) in
@@ -190,7 +191,7 @@ let build_beq_scheme mode kn =
with Not_found -> raise (ParameterWithoutEquality (VarRef x))
in
mkVar eid, Safe_typing.empty_private_constants
- | Cast (x,_,_) -> aux (applist (x,a))
+ | Cast (x,_,_) -> aux (EConstr.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
@@ -206,7 +207,7 @@ let build_beq_scheme mode kn =
in
let args =
Array.append
- (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
+ (Array.of_list (List.map (fun x -> lift lifti (EConstr.Unsafe.to_constr x)) a)) eqa in
if Int.equal (Array.length args) 0 then eq, eff
else mkApp (eq, args), eff
with Not_found -> raise(EqNotFound (ind', fst ind))
@@ -215,10 +216,11 @@ let build_beq_scheme mode kn =
| Prod _ -> raise InductiveWithProduct
| Lambda _-> raise (EqUnknown "abstraction")
| LetIn _ -> raise (EqUnknown "let-in")
- | Const kn ->
- (match Environ.constant_opt_value_in env kn with
- | None -> raise (ParameterWithoutEquality (ConstRef (fst kn)))
- | Some c -> aux (applist (c,a)))
+ | Const (kn, u) ->
+ let u = EConstr.EInstance.kind sigma u in
+ (match Environ.constant_opt_value_in env (kn, u) with
+ | None -> raise (ParameterWithoutEquality (ConstRef kn))
+ | Some c -> aux (EConstr.applist (EConstr.of_constr c,a)))
| Proj _ -> raise (EqUnknown "projection")
| Construct _ -> raise (EqUnknown "constructor")
| Case _ -> raise (EqUnknown "match")
@@ -242,7 +244,7 @@ let build_beq_scheme mode kn =
Cn => match Y with ... end |] part *)
let ci = make_case_info env (fst ind) MatchStyle in
let constrs n = get_constructors env (make_ind_family (ind,
- Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in
+ Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
let ar = Array.make n (Lazy.force ff) in
@@ -262,7 +264,7 @@ let build_beq_scheme mode kn =
nparrec
(nparrec+3+2*nb_cstr_args)
(nb_cstr_args+ndx+1)
- cc
+ (EConstr.of_constr cc)
in
eff := Safe_typing.concat_private eff' !eff;
Array.set eqs ndx
@@ -324,11 +326,12 @@ let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind
(* This function tryies to get the [inductive] between a constr
the constr should be Ind i or App(Ind i,[|args|])
*)
-let destruct_ind c =
- try let u,v = destApp c in
- let indc = destInd u in
+let destruct_ind sigma c =
+ let open EConstr in
+ try let u,v = destApp sigma c in
+ let indc = destInd sigma u in
indc,v
- with DestKO -> let indc = destInd c in
+ with DestKO -> let indc = destInd sigma c in
indc,[||]
(*
@@ -341,11 +344,12 @@ so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
*)
(* used in the leib -> bool side*)
let do_replace_lb mode lb_scheme_key aavoid narg p q =
+ let open EConstr in
let avoid = Array.of_list aavoid in
- let do_arg v offset =
+ let do_arg sigma v offset =
try
let x = narg*offset in
- let s = destVar v in
+ let s = destVar sigma v in
let n = Array.length avoid in
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
@@ -358,19 +362,20 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst v)) in
+ let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_lb")
)))
)
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
- let u,v = destruct_ind type_of_pq
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
+ let sigma = Tacmach.New.project gl in
+ let u,v = destruct_ind sigma type_of_pq
in let lb_type_of_p =
try
- let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in
+ let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in
Proofview.tclUNIT (mkConst c, eff)
with Not_found ->
(* spiwack: the format of this error message should probably
@@ -379,17 +384,18 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(str "Leibniz->boolean:" ++
str "You have to declare the" ++
str "decidability over " ++
- Printer.pr_constr type_of_pq ++
+ Printer.pr_econstr type_of_pq ++
str " first.")
in
Tacticals.New.tclZEROMSG err_msg
in
lb_type_of_p >>= fun (lb_type_of_p,eff) ->
+ Proofview.tclEVARMAP >>= fun sigma ->
let lb_args = Array.append (Array.append
(Array.map (fun x -> x) v)
- (Array.map (fun x -> do_arg x 1) v))
- (Array.map (fun x -> do_arg x 2) v)
- in let app = if Array.equal eq_constr lb_args [||]
+ (Array.map (fun x -> do_arg sigma x 1) v))
+ (Array.map (fun x -> do_arg sigma x 2) v)
+ in let app = if Array.is_empty lb_args
then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
in
Tacticals.New.tclTHENLIST [
@@ -399,11 +405,12 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
(* used in the bool -> leib side *)
let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+ let open EConstr in
let avoid = Array.of_list aavoid in
- let do_arg v offset =
+ let do_arg sigma v offset =
try
let x = narg*offset in
- let s = destVar v in
+ let s = destVar sigma v in
let n = Array.length avoid in
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
@@ -416,7 +423,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
(* if this happen then the args have to be already declared as a
Parameter*)
(
- let mp,dir,lbl = repr_con (fst (destConst v)) in
+ let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
mkConst (make_con mp dir (mk_label (
if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
else ((Label.to_string lbl)^"_bl")
@@ -429,9 +436,10 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
| (t1::q1,t2::q2) ->
Proofview.Goal.enter { enter = begin fun gl ->
let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
- if eq_constr t1 t2 then aux q1 q2
+ let sigma = Tacmach.New.project gl in
+ if EConstr.eq_constr sigma t1 t2 then aux q1 q2
else (
- let u,v = try destruct_ind tt1
+ let u,v = try destruct_ind sigma tt1
(* trick so that the good sequence is returned*)
with e when CErrors.noncritical e -> indu,[||]
in if eq_ind (fst u) ind
@@ -439,7 +447,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
else (
let bl_t1, eff =
try
- let c, eff = find_scheme bl_scheme_key (out_punivs u) (*FIXME*) in
+ let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in
mkConst c, eff
with Not_found ->
(* spiwack: the format of this error message should probably
@@ -448,17 +456,17 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
(str "boolean->Leibniz:" ++
str "You have to declare the" ++
str "decidability over " ++
- Printer.pr_constr tt1 ++
+ Printer.pr_econstr tt1 ++
str " first.")
in
user_err err_msg
in let bl_args =
Array.append (Array.append
(Array.map (fun x -> x) v)
- (Array.map (fun x -> do_arg x 1) v))
- (Array.map (fun x -> do_arg x 2) v )
+ (Array.map (fun x -> do_arg sigma x 1) v))
+ (Array.map (fun x -> do_arg sigma x 2) v )
in
- let app = if Array.equal eq_constr bl_args [||]
+ let app = if Array.is_empty bl_args
then bl_t1 else mkApp (bl_t1,bl_args)
in
Tacticals.New.tclTHENLIST [
@@ -472,21 +480,22 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
| ([],[]) -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
in
- begin try Proofview.tclUNIT (destApp lft)
+ Proofview.tclEVARMAP >>= fun sigma ->
+ begin try Proofview.tclUNIT (destApp sigma lft)
with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
end >>= fun (ind1,ca1) ->
- begin try Proofview.tclUNIT (destApp rgt)
+ begin try Proofview.tclUNIT (destApp sigma rgt)
with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
end >>= fun (ind2,ca2) ->
- begin try Proofview.tclUNIT (out_punivs (destInd ind1))
+ begin try Proofview.tclUNIT (fst (destInd sigma ind1))
with DestKO ->
- begin try Proofview.tclUNIT (fst (fst (destConstruct ind1)))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind1)))
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp1,i1) ->
- begin try Proofview.tclUNIT (out_punivs (destInd ind2))
+ begin try Proofview.tclUNIT (fst (destInd sigma ind2))
with DestKO ->
- begin try Proofview.tclUNIT (fst (fst (destConstruct ind2)))
+ begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind2)))
with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
end
end >>= fun (sp2,i2) ->
@@ -518,7 +527,7 @@ let eqI ind l =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
(str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
- in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff
+ in (if Array.equal Term.eq_constr eA [||] then e else mkApp(e,eA)), eff
(**********************************************************************)
(* Boolean->Leibniz *)
@@ -573,12 +582,10 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
in
let fresh_id s gl =
- Tacmach.New.of_old begin fun gsig ->
- let fresh = fresh_id (!avoid) s gsig in
+ let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
- end gl
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -586,9 +593,9 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
(* try with *)
Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
intro_using freshn ;
- induct_on (mkVar freshn);
+ induct_on (EConstr.mkVar freshn);
intro_using freshm;
- destruct_on (mkVar freshm);
+ destruct_on (EConstr.mkVar freshm);
intro_using freshz;
intros;
Tacticals.New.tclTRY (
@@ -600,10 +607,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
*)
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [
- Simple.apply_in freshz (andb_prop());
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
- destruct_on_as (mkVar freshz)
+ destruct_on_as (EConstr.mkVar freshz)
(IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht);
dl,IntroNaming (IntroIdentifier freshz)]])
end }
@@ -612,11 +619,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Proofview.Goal.nf_enter { enter = begin fun gls ->
- let gl = Proofview.Goal.concl gls in
- match (kind_of_term gl) with
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ let sigma = Tacmach.New.project gl in
+ match EConstr.kind sigma concl with
| App (c,ca) -> (
- match (kind_of_term c) with
+ match EConstr.kind sigma c with
| Ind (indeq, u) ->
if eq_gr (IndRef indeq) Coqlib.glob_eq
then
@@ -656,8 +664,9 @@ let make_bl_scheme mode mind =
let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
let ctx = Evd.make_evar_universe_context (Global.env ()) None in
let side_eff = side_effect_of_mode mode in
+ let bl_goal = EConstr.of_constr bl_goal in
let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
- (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
+ (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
in
([|ans|], ctx), eff
@@ -709,6 +718,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
))), eff
let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
+ let open EConstr in
let list_id = list_id lnamesparrec in
let avoid = ref [] in
let first_intros =
@@ -717,12 +727,10 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- Tacmach.New.of_old begin fun gsig ->
- let fresh = fresh_id (!avoid) s gsig in
+ let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
- end gl
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -730,26 +738,27 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
(* try with *)
Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
intro_using freshn ;
- induct_on (mkVar freshn);
+ induct_on (EConstr.mkVar freshn);
intro_using freshm;
- destruct_on (mkVar freshm);
+ destruct_on (EConstr.mkVar freshm);
intro_using freshz;
intros;
Tacticals.New.tclTRY (
Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
);
- Equality.inj None false None (mkVar freshz,NoBindings);
+ Equality.inj None false None (EConstr.mkVar freshz,NoBindings);
intros; simpl_in_concl;
Auto.default_auto;
Tacticals.New.tclREPEAT (
- Tacticals.New.tclTHENLIST [apply (andb_true_intro());
+ Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
simplest_split ;Auto.default_auto ]
);
- Proofview.Goal.nf_enter { enter = begin fun gls ->
- let gl = Proofview.Goal.concl gls in
+ Proofview.Goal.enter { enter = begin fun gls ->
+ let concl = Proofview.Goal.concl gls in
+ let sigma = Tacmach.New.project gl in
(* assume the goal to be eq (eq_type ...) = true *)
- match (kind_of_term gl) with
- | App(c,ca) -> (match (kind_of_term ca.(1)) with
+ match EConstr.kind sigma concl with
+ | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with
| App(c',ca') ->
let n = Array.length ca' in
do_replace_lb mode lb_scheme_key
@@ -780,6 +789,7 @@ let make_lb_scheme mode mind =
let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
let ctx = Evd.make_evar_universe_context (Global.env ()) None in
let side_eff = side_effect_of_mode mode in
+ let lb_goal = EConstr.of_constr lb_goal in
let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
(compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
in
@@ -865,12 +875,10 @@ let compute_dec_tact ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- Tacmach.New.of_old begin fun gsig ->
- let fresh = fresh_id (!avoid) s gsig in
+ let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
- end gl
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -896,24 +904,24 @@ let compute_dec_tact ind lnamesparrec nparrec =
intros_using fresh_first_intros;
intros_using [freshn;freshm];
(*we do this so we don't have to prove the same goal twice *)
- assert_by (Name freshH) (
+ assert_by (Name freshH) (EConstr.of_constr (
mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
- )
- (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto);
+ ))
+ (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let freshH2 = fresh_id (Id.of_string "H") gl in
- Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
+ Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
(* left *)
Tacticals.New.tclTHENLIST [
simplest_left;
- apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
+ apply (EConstr.of_constr (mkApp(blI,Array.map(fun x->mkVar x) xargs)));
Auto.default_auto
]
;
(*right *)
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let freshH3 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENLIST [
simplest_right ;
@@ -921,15 +929,15 @@ let compute_dec_tact ind lnamesparrec nparrec =
intro;
Equality.subst_all ();
assert_by (Name freshH3)
- (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
+ (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
(Tacticals.New.tclTHENLIST [
- apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
+ apply (EConstr.of_constr (mkApp(lbI,Array.map (fun x->mkVar x) xargs)));
Auto.default_auto
]);
Equality.general_rewrite_bindings_in true
Locus.AllOccurrences true false
(List.hd !avoid)
- ((mkVar (List.hd (List.tl !avoid))),
+ ((EConstr.mkVar (List.hd (List.tl !avoid))),
NoBindings
)
true;
@@ -954,7 +962,7 @@ let make_eq_decidability mode mind =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let side_eff = side_effect_of_mode mode in
let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx
- (compute_dec_goal (ind,u) lnamesparrec nparrec)
+ (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
(compute_dec_tact ind lnamesparrec nparrec)
in
([|ans|], ctx), Safe_typing.empty_private_constants
diff --git a/vernac/class.ml b/vernac/class.ml
index 0dc799014..95114ec39 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -62,7 +62,7 @@ let explain_coercion_error g = function
(* Verifications pour l'ajout d'une classe *)
let check_reference_arity ref =
- if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global_unsafe ref)) then
+ if not (Reductionops.is_arity (Global.env()) Evd.empty (EConstr.of_constr (Global.type_of_global_unsafe ref))) (** FIXME *) then
raise (CoercionError (NotAClass ref))
let check_arity = function
@@ -81,12 +81,13 @@ let check_target clt = function
(* condition d'heritage uniforme *)
-let uniform_cond nargs lt =
+let uniform_cond sigma nargs lt =
+ let open EConstr in
let rec aux = function
| (0,[]) -> true
| (n,t::l) ->
- let t = strip_outer_cast t in
- isRel t && Int.equal (destRel t) n && aux ((n-1),l)
+ let t = strip_outer_cast sigma t in
+ isRel sigma t && Int.equal (destRel sigma t) n && aux ((n-1),l)
| _ -> false
in
aux (nargs,lt)
@@ -120,7 +121,7 @@ let get_source lp source =
let (cl1,u1,lv1) =
match lp with
| [] -> raise Not_found
- | t1::_ -> find_class_type Evd.empty t1
+ | t1::_ -> find_class_type Evd.empty (EConstr.of_constr t1)
in
(cl1,u1,lv1,1)
| Some cl ->
@@ -128,7 +129,7 @@ let get_source lp source =
| [] -> raise Not_found
| t1::lt ->
try
- let cl1,u1,lv1 = find_class_type Evd.empty t1 in
+ let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in
if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1)
else raise Not_found
with Not_found -> aux lt
@@ -138,7 +139,7 @@ let get_target t ind =
if (ind > 1) then
CL_FUN
else
- match pi1 (find_class_type Evd.empty t) with
+ match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
| CL_CONST p when Environ.is_projection p (Global.env ()) ->
CL_PROJ p
| x -> x
@@ -193,20 +194,20 @@ let build_id_coercion idf_opt source poly =
let val_f =
it_mkLambda_or_LetIn
(mkLambda (Name Namegen.default_dependent_ident,
- applistc vs (Context.Rel.to_extended_list 0 lams),
+ applistc vs (Context.Rel.to_extended_list mkRel 0 lams),
mkRel 1))
lams
in
let typ_f =
- it_mkProd_wo_LetIn
- (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t))
+ List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d)
+ (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t))
lams
in
(* juste pour verification *)
let _ =
if not
(Reductionops.is_conv_leq env sigma
- (Typing.unsafe_type_of env sigma val_f) typ_f)
+ (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f))
then
user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
@@ -215,7 +216,7 @@ let build_id_coercion idf_opt source poly =
match idf_opt with
| Some idf -> idf
| None ->
- let cl,u,_ = find_class_type sigma t in
+ let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
@@ -263,7 +264,7 @@ let add_new_coercion_core coef stre poly source target isid =
raise (CoercionError (NoSource source))
in
check_source (Some cls);
- if not (uniform_cond (llp-ind) lvs) then
+ if not (uniform_cond Evd.empty (** FIXME *) (llp-ind) lvs) then
warn_uniform_inheritance coef;
let clt =
try
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c577fe6e3..833719965 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -49,7 +49,7 @@ let set_typeclass_transparency c local b =
let _ =
Hook.set Typeclasses.add_instance_hint_hook
(fun inst path local info poly ->
- let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
+ let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
| IsGlobal gr -> Hints.IsGlobRef gr
in
let info =
@@ -74,7 +74,7 @@ let existing_instance glob g info =
let info = Option.default Hints.empty_hint_info info in
let instance = Global.type_of_global_unsafe c in
let _, r = decompose_prod_assum instance in
- match class_of_constr r with
+ match class_of_constr Evd.empty (EConstr.of_constr r) with
| Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
| None -> user_err ~loc:(loc_of_reference g)
@@ -92,7 +92,7 @@ let type_ctx_instance evars env ctx inst subst =
let t' = substl subst (RelDecl.get_type decl) in
let c', l =
match decl with
- | LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
+ | LocalAssum _ -> EConstr.Unsafe.to_constr (interp_casted_constr_evars env evars (List.hd l) t'), List.tl l
| LocalDef (_,b,_) -> substl subst b, l
in
let d = RelDecl.get_name decl, Some c', t' in
@@ -159,13 +159,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
in
let k, u, cty, ctx', ctx, len, imps, subst =
let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in
+ let ctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) ctx in
let c', imps' = interp_type_evars_impls ~impls env' evars tclass in
+ let c' = EConstr.Unsafe.to_constr c' in
let len = List.length ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum c' in
let ctx'' = ctx' @ ctx in
- let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
- let cl, u = Typeclasses.typeclass_univ_instance k in
+ let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
+ let u = EConstr.EInstance.kind !evars u in
+ let cl, u = Typeclasses.typeclass_univ_instance (k, u) in
let _, args =
List.fold_right (fun decl (args, args') ->
match decl with
@@ -189,7 +192,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars;
- let subst = List.map (Evarutil.nf_evar !evars) subst in
+ let subst = List.map (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar !evars (EConstr.of_constr c))) subst in
if abstract then
begin
let subst = List.fold_left2
@@ -202,7 +205,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
nf t
in
- Pretyping.check_evars env Evd.empty !evars termtype;
+ Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
let pl, ctx = Evd.universe_context ?names:pl !evars in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
(ParameterEntry
@@ -228,6 +231,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
| None -> if List.is_empty k.cl_props then Some (Inl subst) else None
| Some (Inr term) ->
let c = interp_casted_constr_evars env' evars term cty in
+ let c = EConstr.Unsafe.to_constr c in
Some (Inr (c, subst))
| Some (Inl props) ->
let get_id =
@@ -298,7 +302,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let evm, nf = Evarutil.nf_evar_map_universes !evars in
let termtype = nf termtype in
let _ = (* Check that the type is free of evars now. *)
- Pretyping.check_evars env Evd.empty evm termtype
+ Pretyping.check_evars env Evd.empty evm (EConstr.of_constr termtype)
in
let term = Option.map nf term in
if not (Evd.has_undefined evm) && not (Option.is_empty term) then
@@ -334,14 +338,14 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
the refinement manually.*)
let gls = List.rev (Evd.future_goals evm) in
let evm = Evd.reset_future_goals evm in
- Lemmas.start_proof id ?pl kind evm termtype
+ Lemmas.start_proof id ?pl kind evm (EConstr.of_constr termtype)
(Lemmas.mk_hook
(fun _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
- Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
+ Refine.refine { run = fun evm -> Sigma (EConstr.of_constr (Option.get term), evm, Sigma.refl) };
Proofview.Unsafe.tclNEWGOALS gls;
Tactics.New.reduce_after_refine;
]
@@ -370,9 +374,10 @@ let context poly l =
let env = Global.env() in
let evars = ref (Evd.from_env env) in
let _, ((env', fullctx), impls) = interp_context_evars env evars l in
+ let fullctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) fullctx in
let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
let fullctx = Context.Rel.map subst fullctx in
- let ce t = Pretyping.check_evars env Evd.empty !evars t in
+ let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in
let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
let ctx =
try named_of_rel_context fullctx
@@ -387,7 +392,7 @@ let context poly l =
let () = uctx := Univ.ContextSet.empty in
let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
- match class_of_constr t with
+ match class_of_constr !evars (EConstr.of_constr t) with
| Some (rels, ((tc,_), args) as _cl) ->
add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
poly (ConstRef cst));
diff --git a/vernac/command.ml b/vernac/command.ml
index 6eb7037f8..781bf3223 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -45,7 +45,7 @@ let do_universe poly l = Declare.do_universe poly l
let do_constraint poly l = Declare.do_constraint poly l
let rec under_binders env sigma f n c =
- if Int.equal n 0 then f env sigma c else
+ if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
match kind_of_term c with
| Lambda (x,t,c) ->
mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
@@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function
let redfun env sigma c =
let sigma = Sigma.Unsafe.of_evar_map sigma in
let Sigma (c, _, _) = redfun.e_redfun env sigma c in
- c
+ EConstr.Unsafe.to_constr c
in
{ ce with const_entry_body = Future.chain ~pure:true proof_out
(fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
@@ -95,6 +95,7 @@ let interp_definition pl bl p red_option c ctypopt =
let ctx = Evd.make_evar_universe_context env pl in
let evdref = ref (Evd.from_ctx ctx) in
let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
+ let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
let nb_args = List.length ctx in
let imps,pl,ce =
match ctypopt with
@@ -103,6 +104,7 @@ let interp_definition pl bl p red_option c ctypopt =
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
+ let c = EConstr.Unsafe.to_constr c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
let vars = Universes.universes_of_constr body in
@@ -116,9 +118,11 @@ let interp_definition pl bl p red_option c ctypopt =
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
+ let c = EConstr.Unsafe.to_constr c in
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
- let typ = nf (it_mkProd_or_LetIn ty ctx) in
+ let ty = EConstr.Unsafe.to_constr ty in
+ let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in
let beq b1 b2 = if b1 then b2 else not b2 in
let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
(* Check that all implicit arguments inferable from the term
@@ -206,7 +210,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
assert(Univ.ContextSet.is_empty ctx);
let typ = match ce.const_entry_type with
| Some t -> t
- | None -> Retyping.get_type_of env evd c
+ | None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c))
in
Obligations.check_evars env evd;
let obls, _, c, cty =
@@ -263,7 +267,9 @@ match local with
let interp_assumption evdref env impls bl c =
let c = prod_constr_expr c bl in
- interp_type_evars_impls env evdref ~impls c
+ let ty, impls = interp_type_evars_impls env evdref ~impls c in
+ let ty = EConstr.Unsafe.to_constr ty in
+ (ty, impls)
let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
let refs, status, _ =
@@ -303,7 +309,8 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
(* The universe constraints come from the whole telescope. *)
let evd = Evd.nf_constraints evd in
let ctx = Evd.universe_context_set evd in
- let l = List.map (on_pi2 (nf_evar evd)) l in
+ let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in
+ let l = List.map (on_pi2 nf_evar) l in
pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) ->
let t = replace_vars subst t in
let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
@@ -321,6 +328,7 @@ let do_assumptions_bound_univs coe kind nl id pl c =
let evdref = ref (Evd.from_ctx ctx) in
let ty, impls = interp_type_evars_impls env evdref c in
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+ let ty = EConstr.Unsafe.to_constr ty in
let ty = nf ty in
let vars = Universes.universes_of_constr ty in
let evd = Evd.restrict_universe_context !evdref vars in
@@ -398,7 +406,7 @@ let check_all_names_different indl =
| _ -> raise (InductiveError (SameNamesOverlap l))
let mk_mltype_data evdref env assums arity indname =
- let is_ml_type = is_sort env !evdref arity in
+ let is_ml_type = is_sort env !evdref (EConstr.of_constr arity) in
(is_ml_type,indname,assums)
let prepare_param = function
@@ -442,9 +450,10 @@ let interp_ind_arity env evdref ind =
let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
let pseudo_poly = check_anonymous_type c in
- let () = if not (Reduction.is_arity env t) then
+ let () = if not (Reductionops.is_arity env !evdref t) then
user_err ~loc:(constr_loc ind.ind_arity) (str "Not an arity")
in
+ let t = EConstr.Unsafe.to_constr t in
t, pseudo_poly, impls
let interp_cstrs evdref env impls mldata arity ind =
@@ -452,7 +461,7 @@ let interp_cstrs evdref env impls mldata arity ind =
(* Complete conclusions of constructor types if given in ML-style syntax *)
let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
(* Interpret the constructor types *)
- let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
+ let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls %> on_fst EConstr.Unsafe.to_constr) ctyps') in
(cnames, ctyps'', cimpls)
let sign_level env evd sign =
@@ -462,7 +471,7 @@ let sign_level env evd sign =
| LocalDef _ -> lev, push_rel d env
| LocalAssum _ ->
let s = destSort (Reduction.whd_all env
- (nf_evar evd (Retyping.get_type_of env evd (RelDecl.get_type d))))
+ (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))))
in
let u = univ_of_sort s in
(Univ.sup u lev, push_rel d env))
@@ -575,6 +584,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
let _, ((env_params, ctx_params), userimpls) =
interp_context_evars env0 evdref paramsl
in
+ let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in
let indnames = List.map (fun ind -> ind.ind_name) indl in
(* Names of parameters as arguments of the inductive type (defs removed) *)
@@ -584,7 +594,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
(* Interpret the arities *)
let arities = List.map (interp_ind_arity env_params evdref) indl in
- let fullarities = List.map (fun (c, _, _) -> it_mkProd_or_LetIn c ctx_params) arities in
+ let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in
let env_ar = push_types env0 indnames fullarities in
let env_ar_params = push_rel_context ctx_params env_ar in
@@ -619,10 +629,10 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
let ctx_params = Context.Rel.map nf ctx_params in
let evd = !evdref in
let pl, uctx = Evd.universe_context ?names:pl evd in
- List.iter (check_evars env_params Evd.empty evd) arities;
- Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params;
+ List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
+ Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
- List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
+ List.iter (fun c -> check_evars env_ar_params Evd.empty evd (EConstr.of_constr c)) ctyps)
constructors;
(* Build the inductive entries *)
@@ -686,7 +696,7 @@ let is_recursive mie =
let rec is_recursive_constructor lift typ =
match Term.kind_of_term typ with
| Prod (_,arg,rest) ->
- Termops.dependent (mkRel lift) arg ||
+ not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) ||
is_recursive_constructor (lift+1) rest
| LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
| _ -> false
@@ -814,11 +824,11 @@ let warn_non_full_mutual =
(fun (x,xge,y,yge,isfix,rest) ->
non_full_mutual_message x xge y yge isfix rest)
-let check_mutuality env isfix fixl =
+let check_mutuality env evd isfix fixl =
let names = List.map fst fixl in
let preorder =
List.map (fun (id,def) ->
- (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env id' def) names))
+ (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names))
fixl in
let po = partial_order Id.equal preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
@@ -843,15 +853,17 @@ let interp_fix_context env evdref isfix fix =
((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
let interp_fix_ccl evdref impls (env,_) fix =
- interp_type_evars_impls ~impls env evdref fix.fix_type
+ let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in
+ (c, impl)
let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
+ let open EConstr in
Option.map (fun body ->
let env = push_rel_context ctx env_rec in
let body = interp_casted_constr_evars env evdref ~impls body ccl in
it_mkLambda_or_LetIn body ctx) fix.fix_body
-let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
+let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
@@ -891,21 +903,25 @@ let fixsub_module = subtac_dir @ ["Wf"]
let tactics_module = subtac_dir @ ["Tactics"]
let init_reference dir s () = Coqlib.gen_reference "Command" dir s
-let init_constant dir s () = Coqlib.gen_constant "Command" dir s
+let init_constant dir s () = EConstr.of_constr (Coqlib.gen_constant "Command" dir s)
let make_ref l s = init_reference l s
let fix_proto = init_constant tactics_module "fix_proto"
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
let mkSubset name typ prop =
- mkApp (Universes.constr_of_global (delayed_force build_sigma).typ,
+ let open EConstr in
+ mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ),
[| typ; mkLambda (name, typ, prop) |])
let sigT = Lazy.from_fun build_sigma_type
let make_qref s = Qualid (Loc.ghost, qualid_of_string s)
let lt_ref = make_qref "Init.Peano.lt"
-let rec telescope = function
+let rec telescope l =
+ let open EConstr in
+ let open Vars in
+ match l with
| [] -> assert false
| [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1
| LocalAssum (n, t) :: tl ->
@@ -915,7 +931,9 @@ let rec telescope = function
let t = RelDecl.get_type decl in
let pred = mkLambda (RelDecl.get_name decl, t, ty) in
let ty = Universes.constr_of_global (Lazy.force sigT).typ in
+ let ty = EConstr.of_constr ty in
let intro = Universes.constr_of_global (Lazy.force sigT).intro in
+ let intro = EConstr.of_constr intro in
let sigty = mkApp (ty, [|t; pred|]) in
let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
(sigty, pred :: tys, (succ k, intro)))
@@ -925,9 +943,11 @@ let rec telescope = function
(fun pred decl (prev, subst) ->
let t = RelDecl.get_type decl in
let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
+ let p1 = EConstr.of_constr p1 in
let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
- let proj1 = applistc p1 [t; pred; prev] in
- let proj2 = applistc p2 [t; pred; prev] in
+ let p2 = EConstr.of_constr p2 in
+ let proj1 = applist (p1, [t; pred; prev]) in
+ let proj2 = applist (p2, [t; pred; prev]) in
(lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
(List.rev tys) tl (mkRel 1, [])
in ty, (LocalDef (n, last, t) :: subst), constr
@@ -936,9 +956,12 @@ let rec telescope = function
ty, (LocalDef (n, b, t) :: subst), lift 1 term
let nf_evar_context sigma ctx =
- List.map (map_constr (Evarutil.nf_evar sigma)) ctx
+ List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
+ let open EConstr in
+ let open Vars in
+ let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
Coqlib.check_required_library ["Coq";"Program";"Wf"];
let env = Global.env() in
let ctx = Evd.make_evar_universe_context env pl in
@@ -959,23 +982,25 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let error () =
user_err ~loc:(constr_loc r)
~hdr:"Command.build_wellfounded"
- (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
+ (Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
in
try
let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
- match ctx, kind_of_term ar with
- | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
- when Reductionops.is_conv env !evdref t u -> t
+ match ctx, EConstr.kind !evdref ar with
+ | [LocalAssum (_,t); LocalAssum (_,u)], Sort s
+ when Sorts.is_prop (ESorts.kind !evdref s) && Reductionops.is_conv env !evdref t u -> t
| _, _ -> error ()
with e when CErrors.noncritical e -> error ()
in
+ let relargty = EConstr.Unsafe.to_constr relargty in
let measure = interp_casted_constr_evars binders_env evdref measure relargty in
let wf_rel, wf_rel_fun, measure_fn =
let measure_body, measure =
it_mkLambda_or_LetIn measure letbinders,
it_mkLambda_or_LetIn measure binders
in
- let comb = Universes.constr_of_global (delayed_force measure_on_R_ref) in
+ let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in
+ let relargty = EConstr.of_constr relargty in
let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
mkApp (rel, [| subst1 x measure_body;
@@ -990,7 +1015,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
let intern_bl = wfarg 1 :: [arg] in
let _intern_env = push_rel_context intern_bl env in
- let proj = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1 in
+ let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in
let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1003,7 +1028,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
let curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
- let intro = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro in
+ let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in
let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
@@ -1013,23 +1038,23 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
LocalDef (Name recname, body, ty)
in
let fun_bl = intern_fun_binder :: [arg] in
- let lift_lets = Termops.lift_rel_context 1 letbinders in
+ let lift_lets = lift_rel_context 1 letbinders in
let intern_body =
let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
let (r, l, impls, scopes) =
Constrintern.compute_internalization_data env
- Constrintern.Recursive full_arity impls
+ Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls
in
let newimpls = Id.Map.singleton recname
(r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
scopes @ [None]) in
interp_casted_constr_evars (push_rel_context ctx env) evdref
- ~impls:newimpls body (lift 1 top_arity)
+ ~impls:newimpls body (EConstr.Unsafe.to_constr (lift 1 top_arity))
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let def =
- mkApp (Universes.constr_of_global (delayed_force fix_sub_ref),
+ mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
[| argtyp ; wf_rel ;
Evarutil.e_new_evar env evdref
~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
@@ -1045,11 +1070,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
let hook l gr _ =
- let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
+ let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
+ let ty = EConstr.Unsafe.to_constr ty in
let pl, univs = Evd.universe_context ?names:pl !evdref in
(*FIXME poly? *)
- let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
+ let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
@@ -1068,6 +1094,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let hook = Lemmas.mk_hook hook in
let fullcoqc = Evarutil.nf_evar !evdref def in
let fullctyp = Evarutil.nf_evar !evdref typ in
+ let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in
+ let fullctyp = EConstr.Unsafe.to_constr fullctyp in
Obligations.check_evars env !evdref;
let evars, _, evars_def, evars_typ =
Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
@@ -1078,6 +1106,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let interp_recursive isfix fixl notations =
let open Context.Named.Declaration in
+ let open EConstr in
let env = Global.env() in
let fixnames = List.map (fun fix -> fix.fix_name) fixl in
@@ -1098,14 +1127,14 @@ let interp_recursive isfix fixl notations =
let fixctximpenvs, fixctximps = List.split fiximppairs in
let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
- let fixtypes = List.map (nf_evar !evdref) fixtypes in
+ let fixtypes = List.map (fun c -> nf_evar !evdref c) fixtypes in
let fiximps = List.map3
(fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
fixctximps fixcclimps fixctxs in
let rec_sign =
List.fold_left2
(fun env' id t ->
- if Flags.is_program_mode () then
+ if Flags.is_program_mode () then
let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
let fixprot =
try
@@ -1120,6 +1149,8 @@ let interp_recursive isfix fixl notations =
let env_rec = push_named_context rec_sign env in
(* Get interpretation metadatas *)
+ let fixtypes = List.map EConstr.Unsafe.to_constr fixtypes in
+ let fixccls = List.map EConstr.Unsafe.to_constr fixccls in
let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
(* Interp bodies with rollback because temp use of notations/implicit *)
@@ -1134,6 +1165,7 @@ let interp_recursive isfix fixl notations =
(* Instantiate evars and check all are resolved *)
let evd = solve_unif_constraints_with_heuristics env_rec !evdref in
let evd, nf = nf_evars_and_universes evd in
+ let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in
let fixdefs = List.map (Option.map nf) fixdefs in
let fixtypes = List.map nf fixtypes in
let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in
@@ -1145,7 +1177,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
check_evars_are_solved env evd Evd.empty;
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
- check_mutuality env isfix (List.combine fixnames fixdefs)
+ check_mutuality env evd isfix (List.combine fixnames fixdefs)
end
let interp_fixpoint l ntns =
@@ -1165,7 +1197,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
fixnames fixtypes fiximps in
let init_tac =
- Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+ Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
fixdefs) in
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
@@ -1202,7 +1234,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
fixnames fixtypes fiximps in
let init_tac =
- Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+ Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
fixdefs) in
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
@@ -1272,9 +1304,9 @@ let do_program_recursive local p fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
- nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
+ EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
and typ =
- nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
+ EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
diff --git a/vernac/command.mli b/vernac/command.mli
index bccc22ae9..7cd0afeec 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -170,7 +170,7 @@ val do_cofixpoint :
(** Utils *)
-val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
+val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit
val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index e24d5e74f..b898f3e83 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -39,7 +39,7 @@ let detype_param =
let abstract_inductive hyps nparams inds =
let ntyp = List.length inds in
let nhyp = Context.Named.length hyps in
- let args = Context.Named.to_instance (List.rev hyps) in
+ let args = Context.Named.to_instance mkVar (List.rev hyps) in
let args = Array.of_list args in
let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
let inds' =
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f1e0c48f0..dd3ddf4f4 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -57,6 +57,7 @@ let process_vernac_interp_error exn = match fst exn with
mt() in
wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
+ let te = Himsg.map_ptype_error EConstr.of_constr te in
wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 6cff805fc..17bb87f2a 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -29,50 +29,56 @@ module RelDecl = Context.Rel.Declaration
(* This simplifies the typing context of Cases clauses *)
(* hope it does not disturb other typing contexts *)
-let contract env lc =
+let contract env sigma lc =
+ let open EConstr in
let l = ref [] in
let contract_context decl env =
match decl with
- | LocalDef (_,c',_) when isRel c' ->
+ | LocalDef (_,c',_) when isRel sigma c' ->
l := (Vars.substl !l c') :: !l;
env
| _ ->
let t = Vars.substl !l (RelDecl.get_type decl) in
- let decl = decl |> RelDecl.map_name (named_hd env t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in
+ let decl = decl |> RelDecl.map_name (named_hd env sigma t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in
l := (mkRel 1) :: List.map (Vars.lift 1) !l;
push_rel decl env
in
let env = process_rel_context contract_context env in
(env, List.map (Vars.substl !l) lc)
-let contract2 env a b = match contract env [a;b] with
+let contract2 env sigma a b = match contract env sigma [a;b] with
| env, [a;b] -> env,a,b | _ -> assert false
-let contract3 env a b c = match contract env [a;b;c] with
+let contract3 env sigma a b c = match contract env sigma [a;b;c] with
| env, [a;b;c] -> env,a,b,c | _ -> assert false
-let contract4 env a b c d = match contract env [a;b;c;d] with
+let contract4 env sigma a b c d = match contract env sigma [a;b;c;d] with
| env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false
-let contract1_vect env a v =
- match contract env (a :: Array.to_list v) with
+let contract1_vect env sigma a v =
+ match contract env sigma (a :: Array.to_list v) with
| env, a::l -> env,a,Array.of_list l
| _ -> assert false
-let rec contract3' env a b c = function
- | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d)
+let rec contract3' env sigma a b c = function
+ | OccurCheck (evk,d) ->
+ let x,d = contract4 env sigma a b c d in x,OccurCheck(evk, d)
| NotClean ((evk,args),env',d) ->
- let env',d,args = contract1_vect env' d args in
- contract3 env a b c,NotClean((evk,args),env',d)
+ let env',d,args = contract1_vect env' sigma d args in
+ contract3 env sigma a b c,NotClean((evk,args),env',d)
| ConversionFailed (env',t1,t2) ->
- let (env',t1,t2) = contract2 env' t1 t2 in
- contract3 env a b c, ConversionFailed (env',t1,t2)
+ let (env',t1,t2) = contract2 env' sigma t1 t2 in
+ contract3 env sigma a b c, ConversionFailed (env',t1,t2)
| NotSameArgSize | NotSameHead | NoCanonicalStructure
| MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities
- | UnifUnivInconsistency _ as x -> contract3 env a b c, x
+ | UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x
| CannotSolveConstraint ((pb,env',t,u),x) ->
- let env',t,u = contract2 env' t u in
- let y,x = contract3' env a b c x in
+ let t = EConstr.of_constr t in
+ let u = EConstr.of_constr u in
+ let env',t,u = contract2 env' sigma t u in
+ let t = EConstr.Unsafe.to_constr t in
+ let u = EConstr.Unsafe.to_constr u in
+ let y,x = contract3' env sigma a b c x in
y,CannotSolveConstraint ((pb,env',t,u),x)
(** Ad-hoc reductions *)
@@ -82,12 +88,14 @@ let j_nf_betaiotaevar sigma j =
uj_type = Reductionops.nf_betaiota sigma j.uj_type }
let jv_nf_betaiotaevar sigma jl =
- Array.map (j_nf_betaiotaevar sigma) jl
+ Array.map (fun j -> j_nf_betaiotaevar sigma j) jl
(** Printers *)
let pr_lconstr c = quote (pr_lconstr c)
let pr_lconstr_env e s c = quote (pr_lconstr_env e s c)
+let pr_leconstr c = quote (pr_leconstr c)
+let pr_leconstr_env e s c = quote (pr_leconstr_env e s c)
let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)
(** A canonisation procedure for constr such that comparing there
@@ -144,7 +152,8 @@ let explicit_flags =
[print_implicits; print_coercions; print_no_symbol]; (** Then more! *)
[print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ]
-let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags
+let pr_explicit env sigma t1 t2 =
+ pr_explicit_aux env sigma (EConstr.to_constr sigma t1) (EConstr.to_constr sigma t2) explicit_flags
let pr_db env i =
try
@@ -177,9 +186,9 @@ let explain_bad_assumption env sigma j =
brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++
str "because this term is not a type."
-let explain_reference_variables id c =
+let explain_reference_variables sigma id c =
(* c is intended to be a global reference *)
- let pc = pr_global (Globnames.global_of_constr c) in
+ let pc = pr_global (fst (Termops.global_of_constr sigma c)) in
pc ++ strbrk " depends on the variable " ++ pr_id id ++
strbrk " which is not declared in the context."
@@ -196,9 +205,10 @@ let pr_puniverses f env (c,u) =
else mt())
let explain_elim_arity env sigma ind sorts c pj okinds =
- let env = make_all_name_different env in
+ let open EConstr in
+ let env = make_all_name_different env sigma in
let pi = pr_inductive env (fst ind) in
- let pc = pr_lconstr_env env sigma c in
+ let pc = pr_leconstr_env env sigma c in
let msg = match okinds with
| Some(kp,ki,explanation) ->
let pki = pr_sort_family ki in
@@ -211,7 +221,7 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
| WrongArity ->
"wrong arity" in
let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in
- let ppt = pr_lconstr_env env sigma ((strip_prod_assum pj.uj_type)) in
+ let ppt = pr_leconstr_env env sigma (snd (decompose_prod_assum sigma pj.uj_type)) in
hov 0
(str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
@@ -231,10 +241,10 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
let explain_case_not_inductive env sigma cj =
let cj = Evarutil.j_nf_evar sigma cj in
- let env = make_all_name_different env in
- let pc = pr_lconstr_env env sigma cj.uj_val in
- let pct = pr_lconstr_env env sigma cj.uj_type in
- match kind_of_term cj.uj_type with
+ let env = make_all_name_different env sigma in
+ let pc = pr_leconstr_env env sigma cj.uj_val in
+ let pct = pr_leconstr_env env sigma cj.uj_type in
+ match EConstr.kind sigma cj.uj_type with
| Evar _ ->
str "Cannot infer a type for this expression."
| _ ->
@@ -244,18 +254,17 @@ let explain_case_not_inductive env sigma cj =
let explain_number_branches env sigma cj expn =
let cj = Evarutil.j_nf_evar sigma cj in
- let env = make_all_name_different env in
- let pc = pr_lconstr_env env sigma cj.uj_val in
- let pct = pr_lconstr_env env sigma cj.uj_type in
+ let env = make_all_name_different env sigma in
+ let pc = pr_leconstr_env env sigma cj.uj_val in
+ let pct = pr_leconstr_env env sigma cj.uj_type in
str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
str "of type" ++ brk(1,1) ++ pct ++ spc () ++
str "expects " ++ int expn ++ str " branches."
let explain_ill_formed_branch env sigma c ci actty expty =
- let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in
- let c = Evarutil.nf_evar sigma c in
- let env = make_all_name_different env in
- let pc = pr_lconstr_env env sigma c in
+ let simp t = Reductionops.nf_betaiota sigma (Evarutil.nf_evar sigma t) in
+ let env = make_all_name_different env sigma in
+ let pc = pr_leconstr_env env sigma c in
let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ strbrk "the branch for constructor" ++ spc () ++
@@ -265,7 +274,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
let explain_generalization env sigma (name,var) j =
let pe = pr_ne_context_of (str "In environment") env sigma in
- let pv = pr_ltype_env env sigma var in
+ let pv = pr_letype_env env sigma var in
let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in
pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
@@ -277,27 +286,24 @@ let explain_unification_error env sigma p1 p2 = function
| Some e ->
let rec aux p1 p2 = function
| OccurCheck (evk,rhs) ->
- let rhs = Evarutil.nf_evar sigma rhs in
[str "cannot define " ++ quote (pr_existential_key sigma evk) ++
- strbrk " with term " ++ pr_lconstr_env env sigma rhs ++
+ strbrk " with term " ++ pr_leconstr_env env sigma rhs ++
strbrk " that would depend on itself"]
| NotClean ((evk,args),env,c) ->
- let c = Evarutil.nf_evar sigma c in
- let args = Array.map (Evarutil.nf_evar sigma) args in
[str "cannot instantiate " ++ quote (pr_existential_key sigma evk)
- ++ strbrk " because " ++ pr_lconstr_env env sigma c ++
+ ++ strbrk " because " ++ pr_leconstr_env env sigma c ++
strbrk " is not in its scope" ++
(if Array.is_empty args then mt() else
strbrk ": available arguments are " ++
- pr_sequence (pr_lconstr_env env sigma) (List.rev (Array.to_list args)))]
+ pr_sequence (pr_leconstr_env env sigma) (List.rev (Array.to_list args)))]
| NotSameArgSize | NotSameHead | NoCanonicalStructure ->
(* Error speaks from itself *) []
| ConversionFailed (env,t1,t2) ->
- if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then [] else
- let env = make_all_name_different env in
+ if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else
+ let env = make_all_name_different env sigma in
let t1 = Evarutil.nf_evar sigma t1 in
let t2 = Evarutil.nf_evar sigma t2 in
- if not (Term.eq_constr t1 p1) || not (Term.eq_constr t2 p2) then
+ if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then
let t1, t2 = pr_explicit env sigma t1 t2 in
[str "cannot unify " ++ t1 ++ strbrk " and " ++ t2]
else []
@@ -318,11 +324,13 @@ let explain_unification_error env sigma p1 p2 = function
else
[str "universe inconsistency"]
| CannotSolveConstraint ((pb,env,t,u),e) ->
+ let t = EConstr.of_constr t in
+ let u = EConstr.of_constr u in
let t = Evarutil.nf_evar sigma t in
let u = Evarutil.nf_evar sigma u in
- let env = make_all_name_different env in
- (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++
- str " == " ++ pr_lconstr_env env sigma u)
+ let env = make_all_name_different env sigma in
+ (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
+ str " == " ++ pr_leconstr_env env sigma u)
:: aux t u e
| ProblemBeyondCapabilities ->
[]
@@ -333,12 +341,12 @@ let explain_unification_error env sigma p1 p2 = function
prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")"
let explain_actual_type env sigma j t reason =
- let env = make_all_name_different env in
+ let env = make_all_name_different env sigma in
let j = j_nf_betaiotaevar sigma j in
let t = Reductionops.nf_betaiota sigma t in
(** Actually print *)
let pe = pr_ne_context_of (str "In environment") env sigma in
- let pc = pr_lconstr_env env sigma (Environ.j_val j) in
+ let pc = pr_leconstr_env env sigma (Environ.j_val j) in
let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in
let ppreason = explain_unification_error env sigma j.uj_type t reason in
pe ++
@@ -353,7 +361,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let exptyp = Evarutil.nf_evar sigma exptyp in
let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
let rator = Evarutil.j_nf_evar sigma rator in
- let env = make_all_name_different env in
+ let env = make_all_name_different env sigma in
let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
let nargs = Array.length randl in
(* let pe = pr_ne_context_of (str "in environment") env sigma in*)
@@ -379,15 +387,15 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let explain_cant_apply_not_functional env sigma rator randl =
let randl = Evarutil.jv_nf_evar sigma randl in
let rator = Evarutil.j_nf_evar sigma rator in
- let env = make_all_name_different env in
+ let env = make_all_name_different env sigma in
let nargs = Array.length randl in
(* let pe = pr_ne_context_of (str "in environment") env sigma in*)
- let pr = pr_lconstr_env env sigma rator.uj_val in
- let prt = pr_lconstr_env env sigma rator.uj_type in
+ let pr = pr_leconstr_env env sigma rator.uj_val in
+ let prt = pr_leconstr_env env sigma rator.uj_type in
let appl = prvect_with_sep fnl
(fun c ->
- let pc = pr_lconstr_env env sigma c.uj_val in
- let pct = pr_lconstr_env env sigma c.uj_type in
+ let pc = pr_leconstr_env env sigma c.uj_val in
+ let pct = pr_leconstr_env env sigma c.uj_type in
hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
in
str "Illegal application (Non-functional construction): " ++
@@ -405,7 +413,7 @@ let explain_unexpected_type env sigma actual_type expected_type =
str "where" ++ spc () ++ prexp ++ str " was expected."
let explain_not_product env sigma c =
- let c = Evarutil.nf_evar sigma c in
+ let c = EConstr.to_constr sigma c in
let pr = pr_lconstr_env env sigma c in
str "The type of this term is a product" ++ spc () ++
str "while it is expected to be" ++
@@ -414,6 +422,7 @@ let explain_not_product env sigma c =
(* TODO: use the names *)
(* (co)fixpoints *)
let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
+ let pr_lconstr_env env sigma c = pr_leconstr_env env sigma c in
let prt_name i =
match names.(i) with
Name id -> str "Recursive definition of " ++ pr_id id
@@ -428,7 +437,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++
spc () ++ str "which should be an inductive type"
| RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) ->
- let arg_env = make_all_name_different arg_env in
+ let arg_env = make_all_name_different arg_env sigma in
let called =
match names.(j) with
Name id -> pr_id id
@@ -494,7 +503,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
pr_ne_context_of (str "In environment") env sigma ++
st ++ str "." ++ fnl () ++
(try (* May fail with unresolved globals. *)
- let fixenv = make_all_name_different fixenv in
+ let fixenv = make_all_name_different fixenv sigma in
let pvd = pr_lconstr_env fixenv sigma vdefj.(i).uj_val in
str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
with e when CErrors.noncritical e -> mt ())
@@ -502,8 +511,8 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
let explain_ill_typed_rec_body env sigma i names vdefj vargs =
let vdefj = Evarutil.jv_nf_evar sigma vdefj in
let vargs = Array.map (Evarutil.nf_evar sigma) vargs in
- let env = make_all_name_different env in
- let pvd = pr_lconstr_env env sigma vdefj.(i).uj_val in
+ let env = make_all_name_different env sigma in
+ let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in
let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in
str "The " ++
(match vdefj with [|_|] -> mt () | _ -> pr_nth (i+1) ++ spc ()) ++
@@ -512,16 +521,14 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs =
str "while it should be" ++ spc () ++ pv ++ str "."
let explain_cant_find_case_type env sigma c =
- let c = Evarutil.nf_evar sigma c in
- let env = make_all_name_different env in
- let pe = pr_lconstr_env env sigma c in
+ let env = make_all_name_different env sigma in
+ let pe = pr_leconstr_env env sigma c in
str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++
pe ++ str "."
let explain_occur_check env sigma ev rhs =
- let rhs = Evarutil.nf_evar sigma rhs in
- let env = make_all_name_different env in
- let pt = pr_lconstr_env env sigma rhs in
+ let env = make_all_name_different env sigma in
+ let pt = pr_leconstr_env env sigma rhs in
str "Cannot define " ++ pr_existential_key sigma ev ++ str " with term" ++
brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself."
@@ -567,16 +574,16 @@ let rec explain_evar_kind env sigma evk ty = function
| Evar_kinds.SubEvar evk' ->
let evi = Evd.find sigma evk' in
let pc = match evi.evar_body with
- | Evar_defined c -> pr_lconstr_env env sigma (Evarutil.nf_evar sigma c)
+ | Evar_defined c -> pr_leconstr_env env sigma (Evarutil.nf_evar sigma (EConstr.of_constr c))
| Evar_empty -> assert false in
- let ty' = Evarutil.nf_evar sigma evi.evar_concl in
+ let ty' = Evarutil.nf_evar sigma (EConstr.of_constr evi.evar_concl) in
pr_existential_key sigma evk ++ str " of type " ++ ty ++
str " in the partial instance " ++ pc ++
str " found for " ++ explain_evar_kind env sigma evk'
- (pr_lconstr_env env sigma ty') (snd evi.evar_source)
+ (pr_leconstr_env env sigma ty') (snd evi.evar_source)
let explain_typeclass_resolution env sigma evi k =
- match Typeclasses.class_of_constr evi.evar_concl with
+ match Typeclasses.class_of_constr sigma (EConstr.of_constr evi.evar_concl) with
| Some _ ->
let env = Evd.evar_filtered_env evi in
fnl () ++ str "Could not find an instance for " ++
@@ -589,7 +596,7 @@ let explain_placeholder_kind env sigma c e =
| Some (SeveralInstancesFound n) ->
strbrk " (several distinct possible type class instances found)"
| None ->
- match Typeclasses.class_of_constr c with
+ match Typeclasses.class_of_constr sigma (EConstr.of_constr c) with
| Some _ -> strbrk " (no type class instance found)"
| _ -> mt ()
@@ -619,7 +626,7 @@ let explain_wrong_case_info env (ind,u) ci =
spc () ++ pc ++ str "."
let explain_cannot_unify env sigma m n e =
- let env = make_all_name_different env in
+ let env = make_all_name_different env sigma in
let m = Evarutil.nf_evar sigma m in
let n = Evarutil.nf_evar sigma n in
let pm, pn = pr_explicit env sigma m n in
@@ -629,18 +636,19 @@ let explain_cannot_unify env sigma m n e =
str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "."
let explain_cannot_unify_local env sigma m n subn =
- let pm = pr_lconstr_env env sigma m in
- let pn = pr_lconstr_env env sigma n in
- let psubn = pr_lconstr_env env sigma subn in
+ let pm = pr_leconstr_env env sigma m in
+ let pn = pr_leconstr_env env sigma n in
+ let psubn = pr_leconstr_env env sigma subn in
str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++
str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++
psubn ++ str " contains local variables."
let explain_refiner_cannot_generalize env sigma ty =
str "Cannot find a well-typed generalisation of the goal with type: " ++
- pr_lconstr_env env sigma ty ++ str "."
+ pr_leconstr_env env sigma ty ++ str "."
let explain_no_occurrence_found env sigma c id =
+ let c = EConstr.to_constr sigma c in
str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++
str " in " ++
(match id with
@@ -648,20 +656,24 @@ let explain_no_occurrence_found env sigma c id =
| None -> str"the current goal") ++ str "."
let explain_cannot_unify_binding_type env sigma m n =
- let pm = pr_lconstr_env env sigma m in
- let pn = pr_lconstr_env env sigma n in
+ let pm = pr_leconstr_env env sigma m in
+ let pn = pr_leconstr_env env sigma n in
str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
let explain_cannot_find_well_typed_abstraction env sigma p l e =
+ let p = EConstr.to_constr sigma p in
str "Abstracting over the " ++
str (String.plural (List.length l) "term") ++ spc () ++
- hov 0 (pr_enum (pr_lconstr_env env sigma) l) ++ spc () ++
+ hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++
str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env sigma p ++
spc () ++ str "which is ill-typed." ++
(match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
let explain_wrong_abstraction_type env sigma na abs expected result =
+ let abs = EConstr.to_constr sigma abs in
+ let expected = EConstr.to_constr sigma expected in
+ let result = EConstr.to_constr sigma result in
let ppname = match na with Name id -> pr_id id ++ spc () | _ -> mt () in
str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++
pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++
@@ -673,6 +685,7 @@ let explain_abstraction_over_meta _ m n =
pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
let explain_non_linear_unification env sigma m t =
+ let t = EConstr.to_constr sigma t in
strbrk "Cannot unambiguously instantiate " ++
pr_name m ++ str ":" ++
strbrk " which would require to abstract twice on " ++
@@ -680,11 +693,11 @@ let explain_non_linear_unification env sigma m t =
let explain_unsatisfied_constraints env sigma cst =
strbrk "Unsatisfied constraints: " ++
- Univ.pr_constraints (Evd.pr_evd_level sigma) cst ++
+ Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++
spc () ++ str "(maybe a bugged tactic)."
let explain_type_error env sigma err =
- let env = make_all_name_different env in
+ let env = make_all_name_different env sigma in
match err with
| UnboundRel n ->
explain_unbound_rel env sigma n
@@ -695,7 +708,7 @@ let explain_type_error env sigma err =
| BadAssumption c ->
explain_bad_assumption env sigma c
| ReferenceVariables (id,c) ->
- explain_reference_variables id c
+ explain_reference_variables sigma id c
| ElimArity (ind, aritylst, c, pj, okinds) ->
explain_elim_arity env sigma ind aritylst c pj okinds
| CaseNotInductive cj ->
@@ -734,12 +747,16 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1
str "Found nested occurrences of the pattern at positions " ++
int pos1 ++ strbrk " and " ++ pr_position (cl2,pos2) ++ str "."
else
- let ppreason = match e with None -> mt() | Some (c1,c2,e) -> explain_unification_error env sigma c1 c2 (Some e) in
+ let ppreason = match e with
+ | None -> mt()
+ | Some (c1,c2,e) ->
+ explain_unification_error env sigma c1 c2 (Some e)
+ in
str "Found incompatible occurrences of the pattern" ++ str ":" ++
- spc () ++ str "Matched term " ++ pr_lconstr_env env sigma t2 ++
+ spc () ++ str "Matched term " ++ pr_lconstr_env env sigma (EConstr.to_constr sigma t2) ++
strbrk " at position " ++ pr_position (cl2,pos2) ++
strbrk " is not compatible with matched term " ++
- pr_lconstr_env env sigma t1 ++ strbrk " at position " ++
+ pr_lconstr_env env sigma (EConstr.to_constr sigma t1) ++ strbrk " at position " ++
pr_position (cl1,pos1) ++ ppreason ++ str "."
let pr_constraints printenv env sigma evars cstrs =
@@ -759,7 +776,7 @@ let pr_constraints printenv env sigma evars cstrs =
(fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++
str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l
in
- h 0 (pe ++ evs ++ pr_evar_constraints cstrs)
+ h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs)
else
let filter evk _ = Evar.Map.mem evk evars in
pr_evar_map_filter ~with_univs:false filter sigma
@@ -795,23 +812,23 @@ let explain_unsatisfiable_constraints env sigma constr comp =
let explain_pretype_error env sigma err =
let env = Evardefine.env_nf_betaiotaevar sigma env in
- let env = make_all_name_different env in
+ let env = make_all_name_different env sigma in
match err with
| CantFindCaseType c -> explain_cant_find_case_type env sigma c
| ActualTypeNotCoercible (j,t,e) ->
let {uj_val = c; uj_type = actty} = j in
- let (env, c, actty, expty), e = contract3' env c actty t e in
+ let (env, c, actty, expty), e = contract3' env sigma c actty t e in
let j = {uj_val = c; uj_type = actty} in
explain_actual_type env sigma j expty (Some e)
| UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs
| UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp
| VarNotFound id -> explain_var_not_found env id
| UnexpectedType (actual,expect) ->
- let env, actual, expect = contract2 env actual expect in
+ let env, actual, expect = contract2 env sigma actual expect in
explain_unexpected_type env sigma actual expect
| NotProduct c -> explain_not_product env sigma c
| CannotUnify (m,n,e) ->
- let env, m, n = contract2 env m n in
+ let env, m, n = contract2 env sigma m n in
explain_cannot_unify env sigma m n e
| CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn
| CannotGeneralize ty -> explain_refiner_cannot_generalize env sigma ty
@@ -888,7 +905,7 @@ let explain_not_match_error = function
quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
| IncompatibleConstraints cst ->
str " the expected (polymorphic) constraints do not imply " ++
- quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst)
+ quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
let explain_signature_mismatch l spec why =
str "Signature components for label " ++ pr_label l ++
@@ -1004,6 +1021,7 @@ let explain_module_internalization_error = function
(* Typeclass errors *)
let explain_not_a_class env c =
+ let c = EConstr.to_constr Evd.empty c in
pr_constr_env env Evd.empty c ++ str" is not a declared type class."
let explain_unbound_method env cid id =
@@ -1059,7 +1077,7 @@ let explain_non_linear_proof c =
spc () ++ str "because a metavariable has several occurrences."
let explain_meta_in_type c =
- str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++
+ str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr c ++
str " of another meta"
let explain_no_such_hyp id =
@@ -1092,7 +1110,7 @@ let error_ill_formed_inductive env c v =
let error_ill_formed_constructor env id c v nparams nargs =
let pv = pr_lconstr_env env Evd.empty v in
- let atomic = Int.equal (nb_prod c) 0 in
+ let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in
str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++
str "is not valid;" ++ brk(1,1) ++
strbrk (if atomic then "it must be " else "its conclusion must be ") ++
@@ -1111,7 +1129,7 @@ let error_ill_formed_constructor env id c v nparams nargs =
let pr_ltype_using_barendregt_convention_env env c =
(* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
- quote (pr_goal_concl_style_env env Evd.empty c)
+ quote (pr_goal_concl_style_env env Evd.empty (EConstr.of_constr c))
let error_bad_ind_parameters env c n v1 v2 =
let pc = pr_ltype_using_barendregt_convention_env env c in
@@ -1193,7 +1211,8 @@ let explain_recursion_scheme_error = function
(* Pattern-matching errors *)
let explain_bad_pattern env sigma cstr ty =
- let env = make_all_name_different env in
+ let ty = EConstr.to_constr sigma ty in
+ let env = make_all_name_different env sigma in
let pt = pr_lconstr_env env sigma ty in
let pc = pr_constructor env cstr in
str "Found the constructor " ++ pc ++ brk(1,1) ++
@@ -1236,13 +1255,15 @@ let explain_non_exhaustive env pats =
spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats)
let explain_cannot_infer_predicate env sigma typs =
- let env = make_all_name_different env in
+ let inj c = EConstr.to_constr sigma c in
+ let typs = Array.map_to_list (fun (c1, c2) -> (inj c1, inj c2)) typs in
+ let env = make_all_name_different env sigma in
let pr_branch (cstr,typ) =
let cstr,_ = decompose_app cstr in
str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ
in
str "Unable to unify the types found in the branches:" ++
- spc () ++ hov 0 (prlist_with_sep fnl pr_branch (Array.to_list typs))
+ spc () ++ hov 0 (prlist_with_sep fnl pr_branch typs)
let explain_pattern_matching_error env sigma = function
| BadPattern (c,t) ->
@@ -1260,8 +1281,48 @@ let explain_pattern_matching_error env sigma = function
| CannotInferPredicate typs ->
explain_cannot_infer_predicate env sigma typs
+let map_pguard_error f = function
+| NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
+| RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
+| RecursionOnIllegalTerm (n, (env, c), l1, l2) -> RecursionOnIllegalTerm (n, (env, f c), l1, l2)
+| NotEnoughArgumentsForFixCall n -> NotEnoughArgumentsForFixCall n
+| CodomainNotInductiveType c -> CodomainNotInductiveType (f c)
+| NestedRecursiveOccurrences -> NestedRecursiveOccurrences
+| UnguardedRecursiveCall c -> UnguardedRecursiveCall (f c)
+| RecCallInTypeOfAbstraction c -> RecCallInTypeOfAbstraction (f c)
+| RecCallInNonRecArgOfConstructor c -> RecCallInNonRecArgOfConstructor (f c)
+| RecCallInTypeOfDef c -> RecCallInTypeOfDef (f c)
+| RecCallInCaseFun c -> RecCallInCaseFun (f c)
+| RecCallInCaseArg c -> RecCallInCaseArg (f c)
+| RecCallInCasePred c -> RecCallInCasePred (f c)
+| NotGuardedForm c -> NotGuardedForm (f c)
+| ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c)
+
+let map_ptype_error f = function
+| UnboundRel n -> UnboundRel n
+| UnboundVar id -> UnboundVar id
+| NotAType j -> NotAType (on_judgment f j)
+| BadAssumption j -> BadAssumption (on_judgment f j)
+| ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
+| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar)
+| CaseNotInductive j -> CaseNotInductive (on_judgment f j)
+| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
+| NumberBranches (j, n) -> NumberBranches (on_judgment f j, n)
+| IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2)
+| Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j)
+| ActualType (j, t) -> ActualType (on_judgment f j, f t)
+| CantApplyBadType ((n, c1, c2), j, vj) ->
+ CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj)
+| CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv)
+| IllFormedRecBody (ge, na, n, env, jv) ->
+ IllFormedRecBody (map_pguard_error f ge, na, n, env, Array.map (on_judgment f) jv)
+| IllTypedRecBody (n, na, jv, t) ->
+ IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
+| UnsatisfiedConstraints g -> UnsatisfiedConstraints g
+
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
+ let e = map_ptype_error EConstr.of_constr e in
str "The abstracted term" ++ spc () ++
quote (pr_goal_concl_style_env env sigma c) ++
spc () ++ str "is not well typed." ++ fnl () ++
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index ced54fd27..6915ea921 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -40,3 +40,6 @@ val explain_module_error : Modops.module_typing_error -> std_ppcmds
val explain_module_internalization_error :
Modintern.module_internalization_error -> std_ppcmds
+
+val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
+val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index f7e3f0d95..9ba4e46e4 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -319,7 +319,7 @@ let warn_cannot_build_congruence =
strbrk "Cannot build congruence scheme because eq is not found")
let declare_congr_scheme ind =
- if Hipattern.is_equality_type (mkInd ind) then begin
+ if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (** FIXME *) then begin
if
try Coqlib.check_required_library Coqlib.logic_module_name; true
with e when CErrors.noncritical e -> false
@@ -409,7 +409,8 @@ let do_mutual_induction_scheme lnamedepindsort =
in
let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
let declare decl fi lrecref =
- let decltype = Retyping.get_type_of env0 sigma decl in
+ let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
+ let decltype = EConstr.to_constr sigma decltype in
let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
ConstRef cst :: lrecref
@@ -478,7 +479,7 @@ let build_combined_scheme env schemes =
let (c, t) = List.hd defs in
let ctx, ind, nargs = find_inductive t in
(* Number of clauses, including the predicates quantification *)
- let prods = nb_prod t - (nargs + 1) in
+ let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in
let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
let relargs = rel_vect 0 prods in
let concls = List.rev_map
@@ -494,7 +495,7 @@ let build_combined_scheme env schemes =
let ctx, _ =
list_split_rev_at prods
(List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
- let typ = it_mkProd_wo_LetIn concl_typ ctx in
+ let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in
let body = it_mkLambda_or_LetIn concl_bod ctx in
(body, typ)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 409676276..993a2c260 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -108,7 +108,7 @@ let find_mutually_recursive_statements thms =
(* Cofixpoint or fixpoint w/o explicit decreasing argument *)
| None | Some (None, CStructRec) ->
let whnf_hyp_hds = map_rel_context_in_env
- (fun env c -> fst (whd_all_stack env Evd.empty c))
+ (fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c))))
(Global.env()) hyps in
let ind_hyps =
List.flatten (List.map_i (fun i decl ->
@@ -122,8 +122,8 @@ let find_mutually_recursive_statements thms =
[]) 0 (List.rev whnf_hyp_hds)) in
let ind_ccl =
let cclenv = push_rel_context hyps (Global.env()) in
- let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
- match kind_of_term whnf_ccl with
+ let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in
+ match kind_of_term (EConstr.Unsafe.to_constr whnf_ccl) with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
@@ -393,7 +393,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
let rec_tac_initializer finite guard thms snl =
if finite then
- match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
+ match List.map (fun ((id,_),(t,_)) -> (id,EConstr.of_constr t)) thms with
| (id,_)::l -> Tactics.mutual_cofix id l 0
| _ -> assert false
else
@@ -401,7 +401,7 @@ let rec_tac_initializer finite guard thms snl =
let nl = match snl with
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
- in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
+ in match List.map2 (fun ((id,_),(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
@@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook (fun exn -> exn) hook strength ref) thms_data in
- start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+ start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
let start_proof_com ?inference_hook kind thms hook =
let env0 = Global.env () in
@@ -466,7 +466,7 @@ let start_proof_com ?inference_hook kind thms hook =
evdref := solve_remaining_evars flags env !evdref Evd.empty;
let ids = List.map RelDecl.get_name ctx in
(compute_proof_name (pi1 kind) sopt,
- (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
+ (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
(ids, imps @ lift_implicits (List.length ids) imps'),
guard)))
thms in
@@ -518,6 +518,7 @@ let save_proof ?proof = function
| None ->
let pftree = Pfedit.get_pftreestate () in
let id, k, typ = Pfedit.current_proof_statement () in
+ let typ = EConstr.Unsafe.to_constr typ in
let universes = Proof.initial_euctx pftree in
(* This will warn if the proof is complete *)
let pproofs, _univs =
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 39c089be9..681413a29 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -19,17 +19,17 @@ val call_hook :
Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
(** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (types -> unit) -> unit
+val set_start_hook : (EConstr.types -> unit) -> unit
val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val -> types ->
+ ?sign:Environ.named_context_val -> EConstr.types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
unit declaration_hook -> unit
val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val -> types ->
+ ?sign:Environ.named_context_val -> EConstr.types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
(Evd.evar_universe_context option -> unit declaration_hook) -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6f3921903..ea2401b5c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -144,10 +144,11 @@ let trunc_named_context n ctx =
List.firstn (len - n) ctx
let rec chop_product n t =
+ let pop t = Vars.lift (-1) t in
if Int.equal n 0 then Some t
else
match kind_of_term t with
- | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
+ | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None
| _ -> None
let evar_dependencies evm oev =
@@ -266,7 +267,7 @@ let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)
let reduce c =
- Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c
+ EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c))
exception NoObligations of Id.t option
@@ -398,7 +399,7 @@ let subst_deps expand obls deps t =
(Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
let rec prod_app t n =
- match kind_of_term (Termops.strip_outer_cast t) with
+ match kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with
| Prod (_,_,b) -> subst1 n b
| LetIn (_, b, t, b') -> prod_app (subst1 b b') n
| _ ->
@@ -523,7 +524,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
but doing it properly involves delta-reduction, and it finally
doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
- let m = Termops.nb_prod fixtype in
+ let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) in
let ctx = fst (decompose_prod_n_assum m fixtype) in
List.map_i (fun i _ -> i) 0 ctx
@@ -536,8 +537,10 @@ let declare_mutual_definition l =
List.split3
(List.map (fun x ->
let subs, typ = (subst_body true x) in
- let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
- let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
+ let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len (EConstr.of_constr subs)) in
+ let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len (EConstr.of_constr typ)) in
+ let term = EConstr.Unsafe.to_constr term in
+ let typ = EConstr.Unsafe.to_constr typ in
x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
@@ -817,7 +820,7 @@ let rec string_of_list sep f = function
let solve_by_tac name evi t poly ctx =
let id = name in
- let concl = evi.evar_concl in
+ let concl = EConstr.of_constr evi.evar_concl in
(* spiwack: the status is dropped. *)
let (entry,_,ctx') = Pfedit.build_constant_by_tactic
id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
@@ -935,7 +938,7 @@ let rec solve_obligation prg num tac =
Proof_global.make_terminator
(obligation_terminator prg.prg_name num guard hook auto) in
let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
- let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
+ let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in
let _ = Pfedit.by !default_tactic in
Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
diff --git a/vernac/record.ml b/vernac/record.ml
index 288d3391b..8b4b7606f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -66,7 +66,8 @@ let interp_fields_evars env evars impls_env nots l =
List.fold_left2
(fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
let t', impl = interp_type_evars_impls env evars ~impls t in
- let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
+ let b' = Option.map (fun x -> EConstr.Unsafe.to_constr (fst (interp_casted_constr_evars_impls env evars ~impls x t'))) b in
+ let t' = EConstr.Unsafe.to_constr t' in
let impls =
match i with
| Anonymous -> impls
@@ -84,7 +85,7 @@ let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
let univ =
if is_local_assum d then
- let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
+ let s = Retyping.get_sort_of env evars (EConstr.of_constr (RelDecl.get_type d)) in
Univ.sup (univ_of_sort s) univ
else univ
in (push_rel d env, univ))
@@ -114,6 +115,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
in
let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
+ let newps = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) newps in
let t', template = match t with
| Some t ->
let env = push_rel_context newps env0 in
@@ -122,6 +124,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
| CSort (_, Misctypes.GType []) -> true | _ -> false in
let s = interp_type_evars env evars ~impls:empty_internalization_env t in
let sred = Reductionops.whd_all env !evars s in
+ let s = EConstr.Unsafe.to_constr s in
+ let sred = EConstr.Unsafe.to_constr sred in
(match kind_of_term sred with
| Sort s' ->
(if poly then
@@ -164,7 +168,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
let evars, nf = Evarutil.nf_evars_and_universes evars in
let newps = Context.Rel.map nf newps in
let newfs = Context.Rel.map nf newfs in
- let ce t = Pretyping.check_evars env0 Evd.empty evars t in
+ let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
List.iter (iter_constr ce) (List.rev newps);
List.iter (iter_constr ce) (List.rev newfs);
Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs
@@ -271,8 +275,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let ctx = Univ.instantiate_univ_context mib.mind_universes in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
- let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in
- let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*)
+ let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
+ let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
let x = Name binder_name in
let fields = instantiate_possibly_recursive_type indu paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
@@ -365,17 +369,17 @@ let structure_signature ctx =
| [decl] ->
let env = Environ.empty_named_context_val in
let evm = Sigma.Unsafe.of_evar_map evm in
- let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in
+ let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in
let evm = Sigma.to_evar_map evm in
evm
| decl::tl ->
let env = Environ.empty_named_context_val in
let evm = Sigma.Unsafe.of_evar_map evm in
- let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in
+ let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in
let evm = Sigma.to_evar_map evm in
let new_tl = Util.List.map_i
(fun pos decl ->
- RelDecl.map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
+ RelDecl.map_type (fun t -> EConstr.Unsafe.to_constr (Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t))) decl) 1 tl in
deps_to_evar evm new_tl in
deps_to_evar Evd.empty (List.rev ctx)
@@ -384,7 +388,7 @@ open Typeclasses
let declare_structure finite poly ctx id idbuild paramimpls params arity template
fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
- let args = Context.Rel.to_extended_list nfields params in
+ let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let binder_name =
@@ -485,7 +489,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
in
let ctx_context =
List.map (fun decl ->
- match Typeclasses.class_of_constr (RelDecl.get_type decl) with
+ match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
| Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
| None -> None)
params, params
diff --git a/vernac/search.ml b/vernac/search.ml
index 540573843..6279b17ae 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -177,20 +177,20 @@ let prioritize_search seq fn =
(** This function tries to see whether the conclusion matches a pattern. *)
(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
-let rec pattern_filter pat ref env typ =
- let typ = Termops.strip_outer_cast typ in
- if Constr_matching.is_matching env Evd.empty pat typ then true
- else match kind_of_term typ with
+let rec pattern_filter pat ref env sigma typ =
+ let typ = Termops.strip_outer_cast sigma typ in
+ if Constr_matching.is_matching env sigma pat typ then true
+ else match EConstr.kind sigma typ with
| Prod (_, _, typ)
- | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
+ | LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ
| _ -> false
-let rec head_filter pat ref env typ =
- let typ = Termops.strip_outer_cast typ in
- if Constr_matching.is_matching_head env Evd.empty pat typ then true
- else match kind_of_term typ with
+let rec head_filter pat ref env sigma typ =
+ let typ = Termops.strip_outer_cast sigma typ in
+ if Constr_matching.is_matching_head env sigma pat typ then true
+ else match EConstr.kind sigma typ with
| Prod (_, _, typ)
- | LetIn (_, _, _, typ) -> head_filter pat ref env typ
+ | LetIn (_, _, _, typ) -> head_filter pat ref env sigma typ
| _ -> false
let full_name_of_reference ref =
@@ -217,7 +217,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref)
let search_about_filter query gr env typ = match query with
| GlobSearchSubPattern pat ->
- Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat typ
+ Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat (EConstr.of_constr typ)
| GlobSearchString s ->
String.string_contains ~where:(name_of_reference gr) ~what:s
@@ -228,7 +228,7 @@ let search_pattern gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
- pattern_filter pat ref env typ &&
+ pattern_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) &&
blacklist_filter ref env typ
in
let iter ref env typ =
@@ -252,8 +252,8 @@ let search_rewrite gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
- (pattern_filter pat1 ref env typ ||
- pattern_filter pat2 ref env typ) &&
+ (pattern_filter pat1 ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) ||
+ pattern_filter pat2 ref env Evd.empty (EConstr.of_constr typ)) &&
blacklist_filter ref env typ
in
let iter ref env typ =
@@ -267,7 +267,7 @@ let search_by_head gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
- head_filter pat ref env typ &&
+ head_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) &&
blacklist_filter ref env typ
in
let iter ref env typ =
@@ -331,12 +331,12 @@ let interface_search =
toggle (Str.string_match regexp id 0) flag
in
let match_type (pat, flag) =
- toggle (Constr_matching.is_matching env Evd.empty pat constr) flag
+ toggle (Constr_matching.is_matching env Evd.empty pat (EConstr.of_constr constr)) flag
in
let match_subtype (pat, flag) =
toggle
(Constr_matching.is_matching_appsubterm ~closed:false
- env Evd.empty pat constr) flag
+ env Evd.empty pat (EConstr.of_constr constr)) flag
in
let match_module (mdl, flag) =
toggle (Libnames.is_dirpath_prefix_of mdl path) flag
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca03ba3f3..53d49ddbc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -60,7 +60,7 @@ let show_proof () =
(* spiwack: this would probably be cooler with a bit of polishing. *)
let p = Proof_global.give_me_the_proof () in
let pprf = Proof.partial_proof p in
- Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
+ Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
let show_node () =
(* spiwack: I'm have little clue what this function used to do. I deactivated it,
@@ -81,8 +81,8 @@ let show_universes () =
let gls = Proof.V82.subgoals pfts in
let sigma = gls.Evd.sigma in
let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
- Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
- Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
+ Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
+ Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
let show_prooftree () =
(* Spiwack: proof tree is currently not working *)
@@ -103,11 +103,12 @@ let try_print_subgoals () =
(* Simulate the Intro(s) tactic *)
let show_intro all =
+ let open EConstr in
let pf = get_pftreestate() in
let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
if not (List.is_empty gls) then begin
let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
- let l,_= decompose_prod_assum (Termops.strip_outer_cast (pf_concl gl)) in
+ let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
if all then
let lid = Tactics.find_intro_names l gl in
Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid))
@@ -457,11 +458,12 @@ let start_proof_and_print k l hook =
let env = Evd.evar_filtered_env evi in
try
let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in
+ let concl = EConstr.of_constr concl in
if Evarutil.has_undefined_evars sigma concl then raise Exit;
let c, _, ctx =
Pfedit.build_by_tactic env (Evd.evar_universe_context sigma)
concl (Tacticals.New.tclCOMPLETE tac)
- in Evd.set_universe_context sigma ctx, c
+ in Evd.set_universe_context sigma ctx, EConstr.of_constr c
with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
error "The statement obligations could not be resolved \
automatically, write a statement definition first."
@@ -869,6 +871,7 @@ let vernac_set_used_variables e =
let env = Global.env () in
let tys =
List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
+ let tys = List.map EConstr.Unsafe.to_constr tys in
let l = Proof_using.process_expr env e tys in
let vars = Environ.named_context env in
List.iter (fun id ->
@@ -1230,7 +1233,7 @@ let vernac_reserve bl =
let env = Global.env() in
let sigma = Evd.from_env env in
let t,ctx = Constrintern.interp_type env sigma c in
- let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in
+ let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
@@ -1567,6 +1570,7 @@ let get_current_context_of_args = function
let vernac_check_may_eval redexp glopt rc =
let (sigma, env) = get_current_context_of_args glopt in
let sigma', c = interp_open_constr env sigma rc in
+ let c = EConstr.Unsafe.to_constr c in
let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
Evarconv.check_problems_are_solved env sigma';
let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
@@ -1574,14 +1578,16 @@ let vernac_check_may_eval redexp glopt rc =
let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
let c = nf c in
let j =
- if Evarutil.has_undefined_evars sigma' c then
- Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c)
+ if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
+ Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c))
else
(* OK to call kernel which does not support evars *)
- Arguments_renaming.rename_typing env c in
+ Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
+ in
match redexp with
| None ->
- let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
+ let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in
+ let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in
let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
Feedback.msg_notice (print_judgment env sigma' j ++
pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
@@ -1641,7 +1647,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
let natureofid = match decl with
| LocalAssum _ -> "Hypothesis"
| LocalDef (_,bdy,_) ->"Constant (let in)" in
- v 0 (pr_id id ++ str":" ++ pr_constr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
+ v 0 (pr_id id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
++ str natureofid ++ str " of the goal context.")
with (* fallback to globals *)
| NoHyp | Not_found -> print_about ref_or_by_not
@@ -1893,7 +1899,7 @@ let vernac_check_guard () =
try
let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in
Inductiveops.control_only_guard (Goal.V82.env sigma gl)
- pfterm;
+ (EConstr.Unsafe.to_constr pfterm);
(str "The condition holds up to here")
with UserError(_,s) ->
(str ("Condition violated: ") ++s)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 01:27:13 +0000