summaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/Algebra.v2
-rw-r--r--plugins/cc/ccalgo.ml20
-rw-r--r--plugins/cc/ccalgo.mli2
-rw-r--r--plugins/cc/cctac.ml49
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml42
-rw-r--r--plugins/derive/derive.ml4
-rw-r--r--plugins/extraction/CHANGES6
-rw-r--r--plugins/extraction/ExtrHaskellNatInt.v13
-rw-r--r--plugins/extraction/ExtrHaskellNatInteger.v13
-rw-r--r--plugins/extraction/ExtrHaskellNatNum.v35
-rw-r--r--plugins/extraction/ExtrHaskellString.v38
-rw-r--r--plugins/extraction/ExtrHaskellZInt.v24
-rw-r--r--plugins/extraction/ExtrHaskellZInteger.v23
-rw-r--r--plugins/extraction/ExtrHaskellZNum.v21
-rw-r--r--plugins/extraction/extraction.ml3
-rw-r--r--plugins/extraction/mlutil.ml14
-rw-r--r--plugins/extraction/vo.itarget9
-rw-r--r--plugins/firstorder/instances.ml4
-rw-r--r--plugins/firstorder/sequent.ml7
-rw-r--r--plugins/funind/functional_principles_proofs.ml24
-rw-r--r--plugins/funind/functional_principles_types.ml68
-rw-r--r--plugins/funind/functional_principles_types.mli10
-rw-r--r--plugins/funind/g_indfun.ml4244
-rw-r--r--plugins/funind/glob_term_to_relation.ml99
-rw-r--r--plugins/funind/glob_termops.mli4
-rw-r--r--plugins/funind/indfun.ml75
-rw-r--r--plugins/funind/indfun_common.ml13
-rw-r--r--plugins/funind/indfun_common.mli4
-rw-r--r--plugins/funind/invfun.ml26
-rw-r--r--plugins/funind/merge.ml8
-rw-r--r--plugins/funind/recdef.ml32
-rw-r--r--plugins/micromega/mfourier.ml2
-rw-r--r--plugins/omega/coq_omega.ml10
-rw-r--r--plugins/romega/refl_omega.ml8
-rw-r--r--plugins/setoid_ring/newring.ml413
35 files changed, 481 insertions, 488 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index bc5a3900..ee7341a4 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -283,7 +283,7 @@ end.
(** Quotienting a polynomial by the relation X_i^2 ~ X_i *)
-(* Remove the multiple occurences of monomials x_k *)
+(* Remove the multiple occurrences of monomials x_k *)
Fixpoint reduce_aux k p :=
match p with
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 29bca862..97ea5fdc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -129,14 +129,14 @@ type cinfo=
ci_nhyps: int} (* # projectable args *)
let family_eq f1 f2 = match f1, f2 with
-| InProp, InProp
-| InSet, InSet
-| InType, InType -> true
-| _ -> false
+ | Prop Pos, Prop Pos
+ | Prop Null, Prop Null
+ | Type _, Type _ -> true
+ | _ -> false
type term=
Symb of constr
- | Product of sorts_family * sorts_family
+ | Product of sorts * sorts
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -161,7 +161,7 @@ let hash_sorts_family = function
let rec hash_term = function
| Symb c -> combine 1 (hash_constr c)
- | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2)
+ | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
| Eps i -> combine 3 (Id.hash i)
| Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
| Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
@@ -425,8 +425,8 @@ let _B_ = Name (Id.of_string "A")
let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2)
let cc_product s1 s2 =
- mkLambda(_A_,mkSort(Universes.new_sort_in_family s1),
- mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_))
+ mkLambda(_A_,mkSort(s1),
+ mkLambda(_B_,mkSort(s2),_body_))
let rec constr_of_term = function
Symb s-> applist_projection s []
@@ -513,7 +513,7 @@ let rec add_term state t=
Not_found ->
let b=next uf in
let trm = constr_of_term t in
- let typ = pf_type_of state.gls trm in
+ let typ = pf_unsafe_type_of state.gls trm in
let typ = canonize_name typ in
let new_node=
match t with
@@ -836,7 +836,7 @@ let complete_one_class state i=
let _,etyp,rest= destProd typ in
let id = new_state_var etyp state in
app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
- let _c = pf_type_of state.gls
+ let _c = pf_unsafe_type_of state.gls
(constr_of_term (term state.uf pac.cnode)) in
let _args =
List.map (fun i -> constr_of_term (term state.uf i))
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index c72843d5..0dcf3a87 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -30,7 +30,7 @@ type cinfo =
type term =
Symb of constr
- | Product of sorts_family * sorts_family
+ | Product of sorts * sorts
| Eps of Id.t
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8884aef1..068cb25c 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -46,7 +46,7 @@ let whd_delta env=
(* decompose member of equality in an applicative format *)
(** FIXME: evar leak *)
-let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c)
+let sf_of env sigma c = sort_of env (ref sigma) c
let rec decompose_term env sigma t=
match kind_of_term (whd env t) with
@@ -253,9 +253,15 @@ let new_app_global f args k =
let new_refine c = Proofview.V82.tactic (refine c)
+let assert_before n c =
+ Proofview.Goal.enter begin fun gl ->
+ let evm, _ = Tacmach.New.pf_apply type_of gl c in
+ Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
+ end
+
let rec proof_tac p : unit Proofview.tactic =
Proofview.Goal.nf_enter begin fun gl ->
- let type_of t = Tacmach.New.pf_type_of gl t in
+ let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
try (* type_of can raise exceptions *)
match p.p_rule with
Ax c -> exact_check c
@@ -302,9 +308,9 @@ let rec proof_tac p : unit Proofview.tactic =
Tacticals.New.tclFIRST
[Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
reflexivity;
- Proofview.tclZERO (UserError ("Congruence" ,
+ Tacticals.New.tclZEROMSG
(Pp.str
- "I don't know how to handle dependent equality")))]]
+ "I don't know how to handle dependent equality")]]
| Inject (prf,cstr,nargs,argind) ->
let ti=constr_of_term prf.p_lhs in
let tj=constr_of_term prf.p_rhs in
@@ -325,7 +331,7 @@ let refute_tac c t1 t2 p =
Proofview.Goal.nf_enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let intype =
- Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl
+ Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
in
let neweq= new_app_global _eq [|intype;tt1;tt2|] in
let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
@@ -335,14 +341,14 @@ let refute_tac c t1 t2 p =
end
let refine_exact_check c gl =
- let evm, _ = pf_apply e_type_of gl c in
+ let evm, _ = pf_apply type_of gl c in
Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
let convert_to_goal_tac c t1 t2 p =
Proofview.Goal.nf_enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let sort =
- Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl
+ Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
in
let neweq= new_app_global _eq [|sort;tt1;tt2|] in
let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
@@ -367,7 +373,7 @@ let discriminate_tac (cstr,u as cstru) p =
Proofview.Goal.nf_enter begin fun gl ->
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
let intype =
- Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl
+ Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
in
let concl = Proofview.Goal.concl gl in
(* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *)
@@ -376,7 +382,7 @@ let discriminate_tac (cstr,u as cstru) p =
(* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
(* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
let identity = Universes.constr_of_global (Lazy.force _I) in
- (* let trivial=pf_type_of gls identity in *)
+ (* let trivial=pf_unsafe_type_of gls identity in *)
let trivial = Universes.constr_of_global (Lazy.force _True) in
let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in
let outtype = mkSort outtype in
@@ -476,19 +482,28 @@ let congruence_tac depth l =
This isn't particularly related with congruence, apart from
the fact that congruence is called internally.
*)
-
+
+let mk_eq f c1 c2 k =
+ Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+ Proofview.Goal.enter begin
+ fun gl ->
+ let open Tacmach.New in
+ let evm, ty = pf_apply type_of gl c1 in
+ let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
+ let term = mkApp (fc, [| ty; c1; c2 |]) in
+ let evm, _ = type_of (pf_env gl) evm term in
+ Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
+ (k term)
+ end)
+
let f_equal =
Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let type_of = Tacmach.New.pf_type_of gl in
let cut_eq c1 c2 =
try (* type_of can raise an exception *)
- let ty = (* Termops.refresh_universes *) (type_of c1) in
- if eq_constr_nounivs c1 c2 then Proofview.tclUNIT ()
- else
- Tacticals.New.tclTRY (Tacticals.New.tclTHEN
- ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
- (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
+ Tacticals.New.tclTHEN
+ (mk_eq _eq c1 c2 Tactics.cut)
+ (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
Proofview.tclORELSE
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d0b7f34..1a908064 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -125,10 +125,34 @@ let go_to_proof_mode () =
(* closing gaps *)
+(* spiwack: should use [Proofview.give_up] but that would require
+ moving the whole declarative mode into the new proof engine. It
+ will eventually have to be done.
+
+ As far as I can tell, [daimon_tac] is used after a [thus thesis],
+ it will leave uninstantiated variables instead of giving a relevant
+ message at [Qed]. *)
let daimon_tac gls =
set_daimon_flag ();
{it=[];sigma=sig_sig gls;}
+let daimon_instr env p =
+ let (p,(status,_)) =
+ Proof.run_tactic env begin
+ Proofview.tclINDEPENDENT Proofview.give_up
+ end p
+ in
+ p,status
+
+let do_daimon () =
+ let env = Global.env () in
+ let status =
+ Proof_global.with_current_proof begin fun _ p ->
+ daimon_instr env p
+ end
+ in
+ if not status then Pp.feedback Feedback.AddedAxiom else ()
+
(* post-instruction focus management *)
let goto_current_focus () =
@@ -144,7 +168,7 @@ let goto_current_focus_or_top () =
(* return *)
let close_tactic_mode () =
- try goto_current_focus ()
+ try do_daimon ();goto_current_focus ()
with Not_found ->
error "\"return\" cannot be used outside of Declarative Proof Mode."
@@ -165,7 +189,7 @@ let close_block bt pts =
in
match bt,stack with
B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
- (goto_current_focus ())
+ do_daimon ();goto_current_focus ()
| _, Claim::_ ->
error "\"end claim\" expected."
| _, Focus_claim::_ ->
@@ -188,7 +212,7 @@ let close_previous_case pts =
Proof.is_done pts
then
match get_top_stack pts with
- Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
+ Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
| Suppose_case :: Per (et,_,_,_) :: _ ->
goto_current_focus ()
| _ -> error "Not inside a proof per cases or induction."
@@ -196,7 +220,7 @@ let close_previous_case pts =
match get_stack pts with
Per (et,_,_,_) :: _ -> ()
| Suppose_case :: Per (et,_,_,_) :: _ ->
- goto_current_focus ()
+ do_daimon ();goto_current_focus ()
| _ -> error "Not inside a proof per cases or induction."
(* Proof instructions *)
@@ -749,7 +773,7 @@ let rec take_tac wits gls =
match wits with
[] -> tclIDTAC gls
| wit::rest ->
- let typ = pf_type_of gls wit in
+ let typ = pf_unsafe_type_of gls wit in
tclTHEN (thus_tac wit typ []) (take_tac rest) gls
@@ -830,7 +854,7 @@ let start_tree env ind rp =
let build_per_info etype casee gls =
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls casee in
let is_dep = dependent casee concl in
let hd,args = decompose_app (special_whd gls ctyp) in
let (ind,u) =
@@ -845,7 +869,7 @@ let build_per_info etype casee gls =
| _ -> mind.mind_nparams,None in
let params,real_args = List.chop nparams args in
let abstract_obj c body =
- let typ=pf_type_of gls c in
+ let typ=pf_unsafe_type_of gls c in
lambda_create env (typ,subst_term c body) in
let pred= List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term casee concl)) in
@@ -1204,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
let nparams = mind.mind_nparams in
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls casee in
let hd,all_args = decompose_app (special_whd gls ctyp) in
let ind', u = destInd hd in
let _ = assert (eq_ind ind' ind) in (* just in case *)
let params,real_args = List.chop nparams all_args in
let abstract_obj c body =
- let typ=pf_type_of gls c in
+ let typ=pf_unsafe_type_of gls c in
lambda_create env (typ,subst_term c body) in
let elim_pred = List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term casee concl)) in
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c232ae31..d6c29283 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,8 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body)
- : Entries.const_entry_body =
+let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
+ : Safe_typing.private_constants Entries.const_entry_body =
Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
(f b , ctx) , fx
end
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index fbcd01a1..cf97ae3a 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -193,7 +193,7 @@ beginning of files. Possible clashes are dealt with.
in extracted code.
-* A few constants are explicitely declared to be inlined in extracted code.
+* A few constants are explicitly declared to be inlined in extracted code.
For the moment there are:
Wf.Acc_rec
Wf.Acc_rect
@@ -234,12 +234,12 @@ Those two commands enable a precise control of what is inlined and what is not.
Print Extraction Inline.
-Sum up the current state of the table recording the custom inlings
+Sum up the current state of the table recording the custom inlinings
(Extraction (No)Inline).
Reset Extraction Inline.
-Put the table recording the custom inlings back to empty.
+Put the table recording the custom inlinings back to empty.
As a consequence, there is no more need for options inside the commands of
extraction:
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
new file mode 100644
index 00000000..e94e7d42
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatInt.v
@@ -0,0 +1,13 @@
+(** Extraction of [nat] into Haskell's [Int] *)
+
+Require Import Arith.
+Require Import ExtrHaskellNatNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [nat] into [Int] is definitively *not* a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+ *)
+
+Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
+ "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v
new file mode 100644
index 00000000..038f0ed8
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatInteger.v
@@ -0,0 +1,13 @@
+(** Extraction of [nat] into Haskell's [Integer] *)
+
+Require Import Arith.
+Require Import ExtrHaskellNatNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [nat] into [Integer] isn't necessarily a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+*)
+
+Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ]
+ "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
new file mode 100644
index 00000000..244eb85f
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -0,0 +1,35 @@
+(**
+ * Efficient (but uncertified) extraction of usual [nat] functions
+ * into equivalent versions in Haskell's Prelude that are defined
+ * for any [Num] typeclass instances. Useful in combination with
+ * [Extract Inductive nat] that maps [nat] onto a Haskell type that
+ * implements [Num].
+ *)
+
+Require Import Arith.
+Require Import EqNat.
+
+Extract Inlined Constant Nat.add => "(Prelude.+)".
+Extract Inlined Constant Nat.mul => "(Prelude.*)".
+Extract Inlined Constant Nat.max => "Prelude.max".
+Extract Inlined Constant Nat.min => "Prelude.min".
+Extract Inlined Constant Init.Nat.add => "(Prelude.+)".
+Extract Inlined Constant Init.Nat.mul => "(Prelude.*)".
+Extract Inlined Constant Init.Nat.max => "Prelude.max".
+Extract Inlined Constant Init.Nat.min => "Prelude.min".
+Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
+Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
+Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
+Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
+Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
+Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
+
+Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+
+Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". \ No newline at end of file
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
new file mode 100644
index 00000000..3558f4f2
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -0,0 +1,38 @@
+(**
+ * Special handling of ascii and strings for extraction to Haskell.
+ *)
+
+Require Import Ascii.
+Require Import String.
+
+(**
+ * At the moment, Coq's extraction has no way to add extra import
+ * statements to the extracted Haskell code. You will have to
+ * manually add:
+ *
+ * import qualified Data.Bits
+ * import qualified Data.Char
+ *)
+
+Extract Inductive ascii => "Prelude.Char"
+ [ "(\b0 b1 b2 b3 b4 b5 b6 b7 -> Data.Char.chr (
+ (if b0 then Data.Bits.shiftL 1 0 else 0) Prelude.+
+ (if b1 then Data.Bits.shiftL 1 1 else 0) Prelude.+
+ (if b2 then Data.Bits.shiftL 1 2 else 0) Prelude.+
+ (if b3 then Data.Bits.shiftL 1 3 else 0) Prelude.+
+ (if b4 then Data.Bits.shiftL 1 4 else 0) Prelude.+
+ (if b5 then Data.Bits.shiftL 1 5 else 0) Prelude.+
+ (if b6 then Data.Bits.shiftL 1 6 else 0) Prelude.+
+ (if b7 then Data.Bits.shiftL 1 7 else 0)))" ]
+ "(\f a -> f (Data.Bits.testBit (Data.Char.ord a) 0)
+ (Data.Bits.testBit (Data.Char.ord a) 1)
+ (Data.Bits.testBit (Data.Char.ord a) 2)
+ (Data.Bits.testBit (Data.Char.ord a) 3)
+ (Data.Bits.testBit (Data.Char.ord a) 4)
+ (Data.Bits.testBit (Data.Char.ord a) 5)
+ (Data.Bits.testBit (Data.Char.ord a) 6)
+ (Data.Bits.testBit (Data.Char.ord a) 7))".
+Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
+
+Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
+Extract Inlined Constant String.string_dec => "(Prelude.==)".
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v
new file mode 100644
index 00000000..66690851
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZInt.v
@@ -0,0 +1,24 @@
+(** Extraction of [Z] into Haskell's [Int] *)
+
+Require Import ZArith.
+Require Import ExtrHaskellZNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [Z] into [Int] is definitively *not* a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+ *)
+
+Extract Inductive positive => "Prelude.Int" [
+ "(\x -> 2 Prelude.* x Prelude.+ 1)"
+ "(\x -> 2 Prelude.* x)"
+ "1" ]
+ "(\fI fO fH n -> if n Prelude.== 1 then fH () else
+ if Prelude.odd n
+ then fI (n `Prelude.div` 2)
+ else fO (n `Prelude.div` 2))".
+
+Extract Inductive Z => "Prelude.Int" [ "0" "(\x -> x)" "Prelude.negate" ]
+ "(\fO fP fN n -> if n Prelude.== 0 then fO () else
+ if n Prelude.> 0 then fP n else
+ fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v
new file mode 100644
index 00000000..f192f16e
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZInteger.v
@@ -0,0 +1,23 @@
+(** Extraction of [Z] into Haskell's [Integer] *)
+
+Require Import ZArith.
+Require Import ExtrHaskellZNum.
+
+(** Disclaimer: trying to obtain efficient certified programs
+ by extracting [Z] into [Integer] isn't necessarily a good idea.
+ See comments in [ExtrOcamlNatInt.v].
+*)
+
+Extract Inductive positive => "Prelude.Integer" [
+ "(\x -> 2 Prelude.* x Prelude.+ 1)"
+ "(\x -> 2 Prelude.* x)"
+ "1" ]
+ "(\fI fO fH n -> if n Prelude.== 1 then fH () else
+ if Prelude.odd n
+ then fI (n `Prelude.div` 2)
+ else fO (n `Prelude.div` 2))".
+
+Extract Inductive Z => "Prelude.Integer" [ "0" "(\x -> x)" "Prelude.negate" ]
+ "(\fO fP fN n -> if n Prelude.== 0 then fO () else
+ if n Prelude.> 0 then fP n else
+ fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
new file mode 100644
index 00000000..cbbfda75
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -0,0 +1,21 @@
+(**
+ * Efficient (but uncertified) extraction of usual [Z] functions
+ * into equivalent versions in Haskell's Prelude that are defined
+ * for any [Num] typeclass instances. Useful in combination with
+ * [Extract Inductive Z] that maps [Z] onto a Haskell type that
+ * implements [Num].
+ *)
+
+Require Import ZArith.
+Require Import EqNat.
+
+Extract Inlined Constant Z.add => "(Prelude.+)".
+Extract Inlined Constant Z.sub => "(Prelude.-)".
+Extract Inlined Constant Z.mul => "(Prelude.*)".
+Extract Inlined Constant Z.max => "Prelude.max".
+Extract Inlined Constant Z.min => "Prelude.min".
+Extract Inlined Constant Z_ge_lt_dec => "(Prelude.>=)".
+Extract Inlined Constant Z_gt_le_dec => "(Prelude.>)".
+
+Extract Constant Z.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Z.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 080512b2..6ae519ef 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -633,7 +633,8 @@ let rec extract_term env mle mlt c args =
| Construct (cp,u) ->
extract_cons_app env mle mlt cp u args
| Proj (p, c) ->
- extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
+ let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
+ extract_term env mle mlt term args
| Rel n ->
(* As soon as the expected [mlt] for the head is known, *)
(* we unify it with an fresh copy of the stored type of [Rel n]. *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9fdb0205..6fc1195f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -490,8 +490,8 @@ let ast_occurs_itvl k k' t =
ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
with Found -> true
-(* Number of occurences of [Rel 1] in [t], with special treatment of match:
- occurences in different branches aren't added, but we rather use max. *)
+(* Number of occurrences of [Rel 1] in [t], with special treatment of match:
+ occurrences in different branches aren't added, but we rather use max. *)
let nb_occur_match =
let rec nb k = function
@@ -851,7 +851,7 @@ let factor_branches o typ br =
else Some (br_factor, br_set)
end
-(*s If all branches are functions, try to permut the case and the functions. *)
+(*s If all branches are functions, try to permute the case and the functions. *)
let rec merge_ids ids ids' = match ids,ids' with
| [],l -> l
@@ -1127,7 +1127,7 @@ let term_expunge s (ids,c) =
MLlam (Dummy, ast_lift 1 c)
else named_lams ids c
-(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+(*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and
purge the args of [MLrel r] corresponding to a [dummy_name].
It makes eta-expansion if needed. *)
@@ -1351,10 +1351,10 @@ let is_not_strict t =
We expand small terms with at least one non-strict
variable (i.e. a variable that may not be evaluated).
- Futhermore we don't expand fixpoints.
+ Furthermore we don't expand fixpoints.
- Moreover, as mentionned by X. Leroy (bug #2241),
- inling a constant from inside an opaque module might
+ Moreover, as mentioned by X. Leroy (bug #2241),
+ inlining a constant from inside an opaque module might
break types. To avoid that, we require below that
both [r] and its body are globally visible. This isn't
fully satisfactory, since [r] might not be visible (functor),
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index f0489048..9c30c5eb 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,4 +1,11 @@
ExtrHaskellBasic.vo
+ExtrHaskellNatNum.vo
+ExtrHaskellNatInt.vo
+ExtrHaskellNatInteger.vo
+ExtrHaskellZNum.vo
+ExtrHaskellZInt.vo
+ExtrHaskellZInteger.vo
+ExtrHaskellString.vo
ExtrOcamlBasic.vo
ExtrOcamlIntConv.vo
ExtrOcamlBigIntConv.vo
@@ -6,4 +13,4 @@ ExtrOcamlNatInt.vo
ExtrOcamlNatBigInt.vo
ExtrOcamlZInt.vo
ExtrOcamlZBigInt.vo
-ExtrOcamlString.vo \ No newline at end of file
+ExtrOcamlString.vo
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 5912f0a0..c80a8081 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -105,7 +105,7 @@ let mk_open_instance id idc gl m t=
let evmap=Refiner.project gl in
let var_id=
if id==dummy_id then dummy_bvid else
- let typ=pf_type_of gl idc in
+ let typ=pf_unsafe_type_of gl idc in
(* since we know we will get a product,
reduction is not too expensive *)
let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
@@ -154,7 +154,7 @@ let left_instance_tac (inst,id) continue seq=
it_mkLambda_or_LetIn
(mkApp(idc,[|ot|])) rc in
let evmap, _ =
- try Typing.e_type_of (pf_env gl) evmap gt
+ try Typing.type_of (pf_env gl) evmap gt
with e when Errors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7d034db5..a77af03d 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl =
let l = expand_constructor_hints l in
let f gr (seq,gl) =
let gl, c = pf_eapply Evd.fresh_global gl gr in
- let typ=(pf_type_of gl c) in
+ let typ=(pf_unsafe_type_of gl c) in
(add_formula Hyp gr typ seq gl,gl) in
List.fold_right f l (seq,gl)
@@ -209,12 +209,13 @@ open Hints
let extend_with_auto_hints l seq gl=
let seqref=ref seq in
let f p_a_t =
- match repr_auto_tactic p_a_t.code with
+ match repr_hint p_a_t.code with
Res_pf (c,_) | Give_exact (c,_)
| Res_pf_THEN_trivial_fail (c,_) ->
+ let (c, _, _) = c in
(try
let gr = global_of_constr c in
- let typ=(pf_type_of gl c) in
+ let typ=(pf_unsafe_type_of gl c) in
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
| _-> () in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4a832435..169a7060 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -328,7 +328,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
let all_ids = pf_ids_of_hyps g in
let new_ids,_ = list_chop ctxt_size all_ids in
let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
- let evm, _ = pf_apply Typing.e_type_of g to_refine in
+ let evm, _ = pf_apply Typing.type_of g to_refine in
tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
)
in
@@ -543,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
tclIDTAC
in
try
- scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
+ scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
with TOREMOVE ->
thin [hyp_id],[]
@@ -593,7 +593,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
observe_tac "after_introduction" (fun g' ->
(* We get infos on the equations introduced*)
- let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
+ let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
(* compute the new value of the body *)
let new_term_value =
match kind_of_term new_term_value_eq with
@@ -606,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
in
let fun_body =
mkLambda(Anonymous,
- pf_type_of g' term,
+ pf_unsafe_type_of g' term,
Termops.replace_term term (mkRel 1) dyn_infos.info
)
in
@@ -638,7 +638,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
fun g ->
let prov_hid = pf_get_new_id hid g in
let c = mkApp(mkVar hid,args) in
- let evm, _ = pf_apply Typing.e_type_of g c in
+ let evm, _ = pf_apply Typing.type_of g c in
tclTHENLIST[
Refiner.tclEVARS evm;
Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -699,7 +699,7 @@ let build_proof
let dyn_infos = {dyn_info' with info =
mkCase(ci,ct,t,cb)} in
let g_nb_prod = nb_prod (pf_concl g) in
- let type_of_term = pf_type_of g t in
+ let type_of_term = pf_unsafe_type_of g t in
let term_eq =
make_refl_eq (Lazy.force refl_equal) type_of_term t
in
@@ -919,7 +919,7 @@ let generalize_non_dep hyp g =
(* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
let hyps = [hyp] in
let env = Global.env () in
- let hyp_typ = pf_type_of g (mkVar hyp) in
+ let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
let to_revert,_ =
Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
if Id.List.mem hyp hyps
@@ -964,7 +964,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
let (type_ctxt,type_of_f),evd =
- let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f
+ let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
in
decompose_prod_n_assum
(nb_params + nb_args) t,evd
@@ -1034,8 +1034,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
(Global.env ()) !evd
(Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
in
- let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in
- evd:=evd';
+ evd:=evd';
+ let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in
res
in
let nb_intro_to_do = nb_prod (pf_concl g) in
@@ -1414,7 +1414,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
let rewrite =
tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
in
- let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in
+ let _,hrec_concl = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in
let f_app = Array.last (snd (destApp hrec_concl)) in
let f = (fst (destApp f_app)) in
let rec backtrack : tactic =
@@ -1641,7 +1641,7 @@ let prove_principle_for_gen
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *)
(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
(* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1));
-(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
+(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
h_intros (List.rev (acc_rec_arg_id::args_ids));
Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
(* observe_tac "finish" *) (fun gl' ->
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 45e5aaf5..c47602bd 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -274,7 +274,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
let new_princ_name =
next_ident_away_in_goal (Id.of_string "___________princ_________") []
in
- let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in
+ let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
let hook = Lemmas.mk_hook (hook new_principle_type) in
begin
Lemmas.start_proof
@@ -303,7 +303,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
try
let f = funs.(i) in
- let type_sort = Universes.new_sort_in_family InType in
+ let env = Global.env () in
+ let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -317,23 +318,23 @@ let generate_functional_principle (evd: Evd.evar_map ref)
id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
in
let names = ref [new_princ_name] in
- let evd' = !evd in
let hook =
fun new_principle_type _ _ ->
if Option.is_empty sorts
then
(* let id_of_f = Label.to_id (con_label f) in *)
let register_with_sort fam_sort =
- let s = Universes.new_sort_in_family fam_sort in
+ let evd' = Evd.from_env (Global.env ()) in
+ let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
- let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in
+ let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in
+ let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
ignore(
Declare.declare_constant
name
- (Entries.DefinitionEntry ce,
+ (DefinitionEntry ce,
Decl_kinds.IsDefinition (Decl_kinds.Scheme))
);
Declare.definition_message name;
@@ -394,7 +395,7 @@ let get_funs_constant mp dp =
let body = Tacred.cbv_norm_flags
(Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
(Global.env ())
- (Evd.empty)
+ (Evd.from_env (Global.env ()))
body
in
body
@@ -446,7 +447,7 @@ let get_funs_constant mp dp =
exception No_graph_found
exception Found_type of int
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
@@ -478,16 +479,15 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
in
let _ = evd := sigma in
let l_schemes =
- List.map (Typing.type_of env sigma) schemes
+ List.map (Typing.unsafe_type_of env sigma) schemes
in
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x)
)
fas
in
- evd:=sigma;
(* We create the first priciple by tactic *)
let first_type,other_princ_types =
match l_schemes with
@@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
let sorts = Array.of_list sorts in
List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
+ let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = destFix fix in
let other_result =
@@ -585,30 +585,29 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
in
{const with
- Entries.const_entry_body =
- (Future.from_val (Term_typing.mk_pure_proof princ_body));
- Entries.const_entry_type = Some scheme_type
+ const_entry_body =
+ (Future.from_val (Safe_typing.mk_pure_proof princ_body));
+ const_entry_type = Some scheme_type
}
)
other_fun_princ_types
in
const::other_result
-
let build_scheme fas =
- Dumpglob.pause ();
- let evd = (ref Evd.empty) in
+ let evd = (ref (Evd.from_env (Global.env ()))) in
let pconstants = (List.map
(fun (_,f,sort) ->
let f_as_constant =
try
Smartlocate.global_with_alias f
with Not_found ->
- Errors.error ("Cannot find "^ Libnames.string_of_reference f)
+ errorlabstrm "FunInd.build_scheme"
+ (str "Cannot find " ++ Libnames.pr_reference f)
in
let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
- let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in
- let _ = evd := evd' in
+ let _ = evd := evd' in
+ let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in
(destConst f,sort)
)
fas
@@ -621,25 +620,24 @@ let build_scheme fas =
ignore
(Declare.declare_constant
princ_id
- (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+ (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
Declare.definition_message princ_id
)
fas
- bodies_types;
- Dumpglob.continue ()
-
-
+ bodies_types
let build_case_scheme fa =
let env = Global.env ()
- and sigma = Evd.empty in
+ and sigma = (Evd.from_env (Global.env ())) in
(* let id_to_constr id = *)
(* Constrintern.global_reference id *)
(* in *)
- let funs = (fun (_,f,_) ->
- try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
- with Not_found ->
- Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
+ let funs =
+ let (_,f,_) = fa in
+ try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+ with Not_found ->
+ errorlabstrm "FunInd.build_case_scheme"
+ (str "Cannot find " ++ Libnames.pr_reference f) in
let first_fun,u = destConst funs in
let funs_mp,funs_dp,_ = Names.repr_con first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
@@ -656,7 +654,7 @@ let build_case_scheme fa =
in
let sigma, scheme =
(fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in
- let scheme_type = (Typing.type_of env sigma ) scheme in
+ let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in
let sorts =
(fun (_,_,x) ->
Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
@@ -670,14 +668,14 @@ let build_case_scheme fa =
);
*)
generate_functional_principle
- (ref Evd.empty)
+ (ref (Evd.from_env (Global.env ())))
false
scheme_type
(Some ([|sorts|]))
(Some princ_name)
this_block_funs
0
- (prove_princ_for_struct (ref Evd.empty) false 0 [|fst (destConst funs)|])
+ (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|])
in
()
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index f6e5578d..bc082f07 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
open Names
open Term
open Misctypes
@@ -29,7 +37,7 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
exception No_graph_found
val make_scheme : Evd.evar_map ref ->
- (pconstant*glob_sort) list -> Entries.definition_entry list
+ (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list
val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit
val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 043d4328..045beb37 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -247,247 +247,3 @@ END
VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ]
END
-
-
-
-
-
-(* FINDUCTION *)
-
-(* comment this line to see debug msgs *)
-let msg x = () ;; let pr_lconstr c = str ""
- (* uncomment this to see debugging *)
-let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n")
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
-let prNamedConstr s c =
- begin
- msg(str "");
- msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
- msg(str "");
- end
-
-
-
-(** Information about an occurrence of a function call (application)
- inside a term. *)
-type fapp_info = {
- fname: constr; (** The function applied *)
- largs: constr list; (** List of arguments *)
- free: bool; (** [true] if all arguments are debruijn free *)
- max_rel: int; (** max debruijn index in the funcall *)
- onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
-}
-
-
-(** [constr_head_match(a b c) a] returns true, false otherwise. *)
-let constr_head_match u t=
- if isApp u
- then
- let uhd,args= destApp u in
- Constr.equal uhd t
- else false
-
-(** [hdMatchSub inu t] returns the list of occurrences of [t] in
- [inu]. DeBruijn are not pushed, so some of them may be unbound in
- the result. *)
-let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
- let subres =
- match kind_of_term inu with
- | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) ->
- hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
- | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *)
- Array.fold_left
- (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test)
- [] bl
- | _ -> (* Cofix will be wrong *)
- fold_constr
- (fun l cstr ->
- l @ hdMatchSub cstr test) [] inu in
- if not (test inu) then subres
- else
- let f,args = decompose_app inu in
- let freeset = Termops.free_rels inu in
- let max_rel = try Int.Set.max_elt freeset with Not_found -> -1 in
- {fname = f; largs = args; free = Int.Set.is_empty freeset;
- max_rel = max_rel; onlyvars = List.for_all isVar args }
- ::subres
-
-let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-
-let mkEq typ c1 c2 =
- mkApp (make_eq(),[| typ; c1; c2|])
-
-
-let poseq_unsafe idunsafe cstr gl =
- let typ = Tacmach.pf_type_of gl cstr in
- tclTHEN
- (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl))
- (tclTHENFIRST
- (Proofview.V82.of_tactic (Tactics.assert_before Anonymous (mkEq typ (mkVar idunsafe) cstr)))
- (Proofview.V82.of_tactic Tactics.reflexivity))
- gl
-
-
-let poseq id cstr gl =
- let x = Tactics.fresh_id [] id gl in
- poseq_unsafe x cstr gl
-
-(* dirty? *)
-
-let list_constr_largs = ref []
-
-let rec poseq_list_ids_rec lcstr gl =
- match lcstr with
- | [] -> tclIDTAC gl
- | c::lcstr' ->
- match kind_of_term c with
- | Var _ ->
- (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
- | _ ->
- let _ = prstr "c = " in
- let _ = prconstr c in
- let _ = prstr "\n" in
- let typ = Tacmach.pf_type_of gl c in
- let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in
- let x = Tactics.fresh_id [] cname gl in
- let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
- let _ = prstr " list_constr_largs = " in
- let _ = prlistconstr !list_constr_largs in
- let _ = prstr "\n" in
-
- tclTHEN
- (poseq_unsafe x c)
- (poseq_list_ids_rec lcstr')
- gl
-
-let poseq_list_ids lcstr gl =
- let _ = list_constr_largs := [] in
- poseq_list_ids_rec lcstr gl
-
-(** [find_fapp test g] returns the list of [app_info] of all calls to
- functions that satisfy [test] in the conclusion of goal g. Trivial
- repetition (not modulo conversion) are deleted. *)
-let find_fapp (test:constr -> bool) g : fapp_info list =
- let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
- let res =
- List.fold_right (List.add_set Pervasives.(=)) pre_res [] in
- (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
- res)
-
-
-
-(** [finduction id filter g] tries to apply functional induction on
- an occurence of function [id] in the conclusion of goal [g]. If
- [id]=[None] then calls to any function are selected. In any case
- [heuristic] is used to select the most pertinent occurrence. *)
-let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
- (nexttac:Proof_type.tactic) g =
- let test = match oid with
- | Some id ->
- let idref = const_of_id id in
- (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *)
- let idconstr = snd (Evd.fresh_global (Global.env ()) Evd.empty idref) in
- (fun u -> constr_head_match u idconstr) (* select only id *)
- | None -> (fun u -> isApp u) in (* select calls to any function *)
- let info_list = find_fapp test g in
- let ordered_info_list = heuristic info_list in
- prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
- if List.is_empty ordered_info_list then Errors.error "function not found in goal\n";
- let taclist: Proof_type.tactic list =
- List.map
- (fun info ->
- (tclTHEN
- (tclTHEN (poseq_list_ids info.largs)
- (
- fun gl ->
- (functional_induction
- true (applist (info.fname, List.rev !list_constr_largs))
- None None) gl))
- nexttac)) ordered_info_list in
- (* we try each (f t u v) until one does not fail *)
- (* TODO: try also to mix functional schemes *)
- tclFIRST taclist g
-
-
-
-
-(** [chose_heuristic oi x] returns the heuristic for reordering
- (and/or forgetting some elts of) a list of occurrences of
- function calls infos to chose first with functional induction. *)
-let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
- match oi with
- | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
- | None ->
- (* Default heuristic: put first occurrences where all arguments
- are *bound* (meaning already introduced) variables *)
- let ordering x y =
- if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
- else if x.free && x.onlyvars then -1
- else if y.free && y.onlyvars then 1
- else 0 (* both not pertinent *)
- in
- List.sort ordering
-
-
-
-TACTIC EXTEND finduction
- ["finduction" ident(id) natural_opt(oi)] ->
- [
- match oi with
- | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0"
- | _ ->
- let heuristic = chose_heuristic oi in
- Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC)
- ]
-END
-
-
-
-TACTIC EXTEND fauto
- [ "fauto" tactic(tac)] ->
- [
- let heuristic = chose_heuristic None in
- Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac)))
- ]
- |
- [ "fauto" ] ->
- [
- let heuristic = chose_heuristic None in
- Proofview.V82.tactic (finduction None heuristic tclIDTAC)
- ]
-
-END
-
-
-TACTIC EXTEND poseq
- [ "poseq" ident(x) constr(c) ] ->
- [ Proofview.V82.tactic (poseq x c) ]
-END
-
-VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY
- [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
-END
-
-VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
- [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
- "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] ->
- [
- let f1,ctx = Constrintern.interp_constr (Global.env()) Evd.empty
- (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
- let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty
- (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
- let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
- let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
- let ar1 = List.length (fst (decompose_prod f1type)) in
- let ar2 = List.length (fst (decompose_prod f2type)) in
- let _ =
- if not (Int.equal ar1 (List.length cl1)) then
- Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in
- let _ =
- if not (Int.equal ar2 (List.length cl2)) then
- Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in
- Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id
- ]
-END
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 9e3f3986..1b12cd42 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,20 +333,20 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in
- let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in
+ let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
+ let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
Environ.push_named (id,value,typ) env
let add_pat_variables pat typ env : Environ.env =
let rec add_pat_variables env pat typ : Environ.env =
- observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty);
+ observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
match pat with
| PatVar(_,na) -> Environ.push_rel (na,None,typ) env
| PatCstr(_,c,patl,na) ->
let Inductiveops.IndType(indf,indargs) =
- try Inductiveops.find_rectype env Evd.empty typ
+ try Inductiveops.find_rectype env (Evd.from_env env) typ
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
@@ -376,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env =
~init:(env,[])
)
in
- observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty);
+ observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
res
@@ -393,7 +393,7 @@ let rec pattern_to_term_and_type env typ = function
constr
in
let Inductiveops.IndType(indf,indargs) =
- try Inductiveops.find_rectype env Evd.empty typ
+ try Inductiveops.find_rectype env (Evd.from_env env) typ
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
@@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ = function
Array.to_list
(Array.init
(cst_narg - List.length patternl)
- (fun i -> Detyping.detype false [] env Evd.empty csta.(i))
+ (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i))
)
in
let patl_as_term =
@@ -486,9 +486,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
a pseudo value "v1 ... vn".
The "value" of this branch is then simply [res]
*)
- let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
- let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
- let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in
+ let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
+ let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+ let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
let new_avoid = res::args_res.to_avoid in
let res_rt = mkGVar res in
@@ -594,8 +594,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
and combine the two result
*)
let v_res = build_entry_lc env funnames avoid v in
- let v_as_constr,ctx = Pretyping.understand env Evd.empty v in
- let v_type = Typing.type_of env Evd.empty v_as_constr in
+ let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
+ let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
let new_env =
match n with
Anonymous -> env
@@ -610,10 +610,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let make_discr = make_discr_match brl in
build_entry_lc_from_case env funnames make_discr el brl avoid
| GIf(_,b,(na,e_option),lhs,rhs) ->
- let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
- let b_typ = Typing.type_of env Evd.empty b_as_constr in
+ let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
- try Inductiveops.find_inductive env Evd.empty b_typ
+ try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
errorlabstrm "" (str "Cannot find the inductive associated to " ++
Printer.pr_glob_constr b ++ str " in " ++
@@ -642,10 +642,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
)
nal
in
- let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
- let b_typ = Typing.type_of env Evd.empty b_as_constr in
+ let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
- try Inductiveops.find_inductive env Evd.empty b_typ
+ try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
errorlabstrm "" (str "Cannot find the inductive associated to " ++
Printer.pr_glob_constr b ++ str " in " ++
@@ -689,8 +689,8 @@ and build_entry_lc_from_case env funname make_discr
in
let types =
List.map (fun (case_arg,_) ->
- let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in
- Typing.type_of env Evd.empty case_arg_as_constr
+ let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
+ Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr
) el
in
(****** The next works only if the match is not dependent ****)
@@ -737,11 +737,11 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
List.fold_right
(fun id acc ->
let typ_of_id =
- Typing.type_of env_with_pat_ids Evd.empty (mkVar id)
+ Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id)
in
let raw_typ_of_id =
Detyping.detype false []
- env_with_pat_ids Evd.empty typ_of_id
+ env_with_pat_ids (Evd.from_env env) typ_of_id
in
mkGProd (Name id,raw_typ_of_id,acc))
pat_ids
@@ -785,15 +785,15 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
List.map3
(fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
- let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in
+ let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
let pat_as_term = pattern_to_term pat in
List.fold_right
(fun id acc ->
if Id.Set.mem id this_pat_ids
then (Prod (Name id),
- let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
+ let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in
let raw_typ_of_id =
- Detyping.detype false [] new_env Evd.empty typ_of_id
+ Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
in
raw_typ_of_id
)::acc
@@ -894,7 +894,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let new_t =
mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
in
- let t',ctx = Pretyping.understand env Evd.empty new_t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -914,7 +914,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
try
observe (str "computing new type for eq : " ++ pr_glob_constr rt);
let t' =
- try fst (Pretyping.understand env Evd.empty t)(*FIXME*)
+ try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
with e when Errors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
@@ -937,7 +937,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkGProd(n,t,new_b),id_to_exclude
with Continue ->
let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
- let ty',ctx = Pretyping.understand env Evd.empty ty in
+ let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
let ind,args' = Inductive.find_inductive env ty' in
let mib,_ = Global.lookup_inductive (fst ind) in
let nparam = mib.Declarations.mind_nparams in
@@ -949,7 +949,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype false []
- env Evd.empty
+ env (Evd.from_env env)
p) params)@(Array.to_list
(Array.make
(List.length args' - nparam)
@@ -959,7 +959,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
in
observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
- let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in
+ let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
observe (str " computing new type for jmeq : done") ;
let new_args =
match kind_of_term eq'_as_constr with
@@ -978,12 +978,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| Name id' ->
(id',Detyping.detype false []
env
- Evd.empty
+ (Evd.from_env env)
arg)::acc
else if isVar var_as_constr
then (destVar var_as_constr,Detyping.detype false []
env
- Evd.empty
+ (Evd.from_env env)
arg)::acc
else acc
)
@@ -1009,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
if is_in_b then b else replace_var_by_term id rt b
in
let new_env =
- let t',ctx = Pretyping.understand env Evd.empty eq' in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
Environ.push_rel (n,None,t') env
in
let new_b,id_to_exclude =
@@ -1047,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
else raise Continue
with Continue ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t',ctx = Pretyping.understand env Evd.empty t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1063,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
end
| _ ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t',ctx = Pretyping.understand env Evd.empty t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1082,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
- let t',ctx = Pretyping.understand env Evd.empty t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
match n with
| Name id ->
let new_env = Environ.push_rel (n,None,t') env in
@@ -1104,8 +1104,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| GLetIn(_,n,t,b) ->
begin
let not_free_in_t id = not (is_free_in id t) in
- let t',ctx = Pretyping.understand env Evd.empty t in
- let type_t' = Typing.type_of env Evd.empty t' in
+ let evd = (Evd.from_env env) in
+ let t',ctx = Pretyping.understand env evd t in
+ let evd = Evd.from_ctx ctx in
+ let type_t' = Typing.unsafe_type_of env evd t' in
let new_env = Environ.push_rel (n,Some t',type_t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1129,7 +1131,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
args (crossed_types)
depth t
in
- let t',ctx = Pretyping.understand env Evd.empty new_t in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
let new_env = Environ.push_rel (na,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1255,7 +1257,7 @@ let do_build_inductive
let evd,env =
Array.fold_right2
(fun id c (evd,env) ->
- let evd,t = Typing.e_type_of env evd (mkConstU c) in
+ let evd,t = Typing.type_of env evd (mkConstU c) in
evd,
Environ.push_named (id,None,t)
(* try *)
@@ -1297,7 +1299,7 @@ let do_build_inductive
let rel_arities = Array.mapi rel_arity funsargs in
Util.Array.fold_left2 (fun env rel_name rel_ar ->
Environ.push_named (rel_name,None,
- fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities
+ fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities
in
(* and of the real constructors*)
let constr i res =
@@ -1395,7 +1397,7 @@ let do_build_inductive
(rel_constructors)
in
let rel_ind i ext_rel_constructors =
- ((Loc.ghost,relnames.(i)),
+ (((Loc.ghost,relnames.(i)), None),
rel_params,
Some rel_arities.(i),
ext_rel_constructors),[]
@@ -1460,8 +1462,17 @@ let do_build_inductive
let build_inductive evd funconstants funsargs returned_types rtl =
+ let pu = !Detyping.print_universes in
+ let cu = !Constrextern.print_universes in
try
- do_build_inductive evd funconstants funsargs returned_types rtl
- with e when Errors.noncritical e -> raise (Building_graph e)
+ Detyping.print_universes := true;
+ Constrextern.print_universes := true;
+ do_build_inductive evd funconstants funsargs returned_types rtl;
+ Detyping.print_universes := pu;
+ Constrextern.print_universes := cu
+ with e when Errors.noncritical e ->
+ Detyping.print_universes := pu;
+ Constrextern.print_universes := cu;
+ raise (Building_graph e)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 0f10636f..179e8fe8 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -6,7 +6,7 @@ open Misctypes
val get_pattern_id : cases_pattern -> Id.t list
(* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
- [pat] must not contain occurences of anonymous pattern
+ [pat] must not contain occurrences of anonymous pattern
*)
val pattern_to_term : cases_pattern -> glob_constr
@@ -64,7 +64,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr
(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t.
the result does not share variables with [avoid]. This function create
- a fresh variable for each occurence of the anonymous pattern.
+ a fresh variable for each occurrence of the anonymous pattern.
Also returns a mapping from old variables to new ones and the concatenation of
[avoid] with the variables appearing in the result.
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e211b688..3dbd4380 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -27,7 +27,6 @@ let choose_dest_or_ind scheme_info =
Tactics.induction_destruct (is_rec_info scheme_info) false
let functional_induction with_clean c princl pat =
- Dumpglob.pause ();
let res =
let f,args = decompose_app c in
fun g ->
@@ -72,11 +71,11 @@ let functional_induction with_clean c princl pat =
errorlabstrm "" (str "Cannot find induction principle for "
++Printer.pr_lconstr (mkConst c') )
in
- (princ,NoBindings, Tacmach.pf_type_of g' princ,g')
+ (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
| _ -> raise (UserError("",str "functional induction must be used with a function" ))
end
| Some ((princ,binding)) ->
- princ,binding,Tacmach.pf_type_of g princ,g
+ princ,binding,Tacmach.pf_unsafe_type_of g princ,g
in
let princ_infos = Tactics.compute_elim_sig princ_type in
let args_as_induction_constr =
@@ -123,9 +122,7 @@ let functional_induction with_clean c princl pat =
(args_as_induction_constr,princ')))
subst_and_reduce
g'
- in
- Dumpglob.continue ();
- res
+ in res
let rec abstract_glob_constr c = function
| [] -> c
@@ -145,15 +142,14 @@ let interp_casted_constr_with_implicits env sigma impls c =
let build_newrecursive
lnameargsardef =
- let env0 = Global.env()
- and sigma = Evd.empty
- in
+ let env0 = Global.env() in
+ let sigma = Evd.from_env env0 in
let (rec_sign,rec_impls) =
List.fold_left
- (fun (env,impls) ((_,recname),bl,arityc,_) ->
+ (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
- let evdref = ref (Evd.from_env env0) in
+ let evdref = ref (Evd.from_env env0) in
let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
(Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
@@ -228,7 +224,7 @@ let process_vernac_interp_error e =
let derive_inversion fix_names =
try
- let evd' = Evd.empty in
+ let evd' = Evd.from_env (Global.env ()) in
(* we first transform the fix_names identifier into their corresponding constant *)
let evd',fix_names_as_constant =
List.fold_right
@@ -323,7 +319,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof
(continue_proof : int -> Names.constant array -> Term.constr array -> int ->
Tacmach.tactic) : unit =
- let names = List.map (function ((_, name),_,_,_,_),_ -> name) fix_rec_l in
+ let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
@@ -343,7 +339,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
locate_ind
f_R_mut)
in
- let fname_kn ((fname,_,_,_,_),_) =
+ let fname_kn (((fname,_),_,_,_,_),_) =
let f_ref = Ident fname in
locate_with_msg
(pr_reference f_ref++str ": Not an inductive type!")
@@ -355,9 +351,11 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
List.map_i
(fun i x ->
let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
- let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in
- let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in
- let _ = evd := evd' in
+ let env = Global.env () in
+ let evd = ref (Evd.from_env env) in
+ let evd',uprinc = Evd.fresh_global env !evd princ in
+ let _ = evd := evd' in
+ let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
Functional_principles_types.generate_functional_principle
evd
interactive_proof
@@ -380,21 +378,21 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
match fixpoint_exprl with
- | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+ | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
Command.do_definition
fname
- (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition)
+ (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+ (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
evd,((destConst c)::l)
)
- (Evd.empty,[])
+ (Evd.from_env (Global.env ()),[])
fixpoint_exprl
in
evd,List.rev rev_pconstants
@@ -402,13 +400,13 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+ (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
evd,((destConst c)::l)
)
- (Evd.empty,[])
+ (Evd.from_env (Global.env ()),[])
fixpoint_exprl
in
evd,List.rev rev_pconstants
@@ -594,9 +592,9 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in
+ let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
let constr_expr_typel =
- with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) Evd.empty)) typel in
+ with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in
let fixpoint_exprl_with_new_bl =
List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
@@ -614,7 +612,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let _is_struct =
match fixpoint_exprl with
| [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- let ((((_,name),_,args,types,body)),_) as fixpoint_expr =
+ let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -625,7 +623,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let using_lemmas = [] in
let pre_hook pconstants =
generate_principle
- (ref (Evd.empty))
+ (ref (Evd.from_env (Global.env ())))
pconstants
on_error
true
@@ -638,7 +636,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
false
|[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- let ((((_,name),_,args,types,body)),_) as fixpoint_expr =
+ let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -649,7 +647,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
let pre_hook pconstants =
generate_principle
- (ref Evd.empty)
+ (ref (Evd.from_env (Global.env ())))
pconstants
on_error
true
@@ -672,7 +670,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
fixpoint_exprl;
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names =
- List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl
+ List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
in
(* ok all the expressions are structural *)
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -680,7 +678,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let evd,pconstants =
if register_built
then register_struct is_rec fixpoint_exprl
- else (Evd.empty,pconstants)
+ else (Evd.from_env (Global.env ()),pconstants)
in
let evd = ref evd in
generate_principle
@@ -830,15 +828,15 @@ let make_graph (f_ref:global_reference) =
end
| _ -> raise (UserError ("", str "Not a function reference") )
in
- Dumpglob.pause ();
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom !"
| Some body ->
let env = Global.env () in
+ let sigma = Evd.from_env env in
let extern_body,extern_type =
with_full_print (fun () ->
- (Constrextern.extern_constr false env Evd.empty body,
- Constrextern.extern_type false env Evd.empty
+ (Constrextern.extern_constr false env sigma body,
+ Constrextern.extern_type false env sigma
((*FIXME*) Typeops.type_of_constant_type env c_body.const_type)
)
)
@@ -867,22 +865,21 @@ let make_graph (f_ref:global_reference) =
)
in
let b' = add_args (snd id) new_args b in
- (((id, ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ ((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixexprl
in
l
| _ ->
let id = Label.to_id (con_label c) in
- [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+ [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
let mp,dp,_ = repr_con c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
- expr_list);
- Dumpglob.continue ()
+ (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
+ expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 738ade8c..aa47e261 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,9 @@ let const_of_id id =
qualid_of_reference (Libnames.Ident (Loc.ghost,id))
in
try Constrintern.locate_reference princ_ref
- with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
+ with Not_found ->
+ Errors.errorlabstrm "IndFun.const_of_id"
+ (str "cannot find " ++ Nameops.pr_id id)
let def_of_const t =
match (Term.kind_of_term t) with
@@ -147,7 +149,7 @@ let get_locality = function
| Global -> false
let save with_clean id const (locality,_,kind) hook =
- let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
+ let fix_exn = Future.fix_exn_of const.const_entry_body in
let l,r = match locality with
| Discharge when Lib.sections_are_opened () ->
let k = Kindops.logical_kind_of_goal_kind kind in
@@ -178,9 +180,10 @@ let get_proof_clean do_reduce =
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
- and old_contextual_implicit_args = Impargs.is_contextual_implicit_args ()
- in
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
let old_rawprint = !Flags.raw_print in
+ let old_printuniverses = !Constrextern.print_universes in
+ Constrextern.print_universes := true;
Flags.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
@@ -193,6 +196,7 @@ let with_full_print f a =
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
+ Constrextern.print_universes := old_printuniverses;
Dumpglob.continue ();
res
with
@@ -201,6 +205,7 @@ let with_full_print f a =
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
+ Constrextern.print_universes := old_printuniverses;
Dumpglob.continue ();
raise reraise
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 10daf6e8..23f1da1b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val const_of_id: Id.t -> Globnames.global_reference(* constantyes *)
val jmeq : unit -> Term.constr
val jmeq_refl : unit -> Term.constr
-val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind ->
unit Lemmas.declaration_hook Ephemeron.key -> unit
(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
@@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind ->
*)
val get_proof_clean : bool ->
Names.Id.t *
- (Entries.definition_entry * Decl_kinds.goal_kind)
+ (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d10924f8..d9794014 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -127,8 +127,8 @@ let generate_type evd g_to_f f graph i =
let evd',graph =
Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd graph)))
in
- let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in
evd:=evd';
+ let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
let ctxt,_ = decompose_prod_assum graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -193,7 +193,7 @@ let find_induction_principle evd f =
| None -> raise Not_found
| Some rect_lemma ->
let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in
- let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+ let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
evd:=evd';
rect_lemma,typ
@@ -296,7 +296,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let constructor_args g =
List.fold_right
(fun hid acc ->
- let type_of_hid = pf_type_of g (mkVar hid) in
+ let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
match kind_of_term type_of_hid with
| Prod(_,_,t') ->
begin
@@ -440,7 +440,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
"functional_induction" (
(fun gl ->
let term = mkApp (mkVar principle_id,Array.of_list bindings) in
- let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true) gl term in
+ let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl term in
Proofview.V82.of_tactic (apply term) gl')
))
(fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -577,7 +577,7 @@ let rec reflexivity_with_destruct_cases g =
match sc with
None -> tclIDTAC g
| Some id ->
- match kind_of_term (pf_type_of g (mkVar id)) with
+ match kind_of_term (pf_unsafe_type_of g (mkVar id)) with
| App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -642,7 +642,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
(* We get the constant and the principle corresponding to this lemma *)
let f = funcs.(i) in
let graph_principle = nf_zeta schemes.(i) in
- let princ_type = pf_type_of g graph_principle in
+ let princ_type = pf_unsafe_type_of g graph_principle in
let princ_infos = Tactics.compute_elim_sig princ_type in
(* Then we get the number of argument of the function
and compute a fresh name for each of them
@@ -760,7 +760,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let funs_constr = Array.map mkConstU funs in
States.with_state_protection_on_exception
(fun () ->
- let evd = ref Evd.empty in
+ let env = Global.env () in
+ let evd = ref (Evd.from_env env) in
let graphs_constr = Array.map mkInd graphs in
let lemmas_types_infos =
Util.Array.map2_i
@@ -772,7 +773,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
- let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in
+ let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in
let type_of_lemma = nf_zeta type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
type_of_lemma,type_info
@@ -829,7 +830,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
)
funs;
- (* let evd = ref Evd.empty in *)
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
@@ -875,7 +875,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
i*)
let lem_id = mk_complete_id f_id in
Lemmas.start_proof lem_id
- (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd
+ (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
(fst lemmas_types_infos.(i))
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
@@ -900,7 +900,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
*)
let revert_graph kn post_tac hid g =
- let typ = pf_type_of g (mkVar hid) in
+ let typ = pf_unsafe_type_of g (mkVar hid) in
match kind_of_term typ with
| App(i,args) when isInd i ->
let ((kn',num) as ind'),u = destInd i in
@@ -951,7 +951,7 @@ let revert_graph kn post_tac hid g =
let functional_inversion kn hid fconst f_correct : tactic =
fun g ->
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in
- let type_of_h = pf_type_of g (mkVar hid) in
+ let type_of_h = pf_unsafe_type_of g (mkVar hid) in
match kind_of_term type_of_h with
| App(eq,args) when eq_constr eq (make_eq ()) ->
let pre_tac,f_args,res =
@@ -1003,7 +1003,7 @@ let invfun qhyp f g =
Proofview.V82.of_tactic begin
Tactics.try_intros_until
(fun hid -> Proofview.V82.tactic begin fun g ->
- let hyp_typ = pf_type_of g (mkVar hid) in
+ let hyp_typ = pf_unsafe_type_of g (mkVar hid) in
match kind_of_term hyp_typ with
| App(eq,args) when eq_constr eq (make_eq ()) ->
begin
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ea699580..e3455e77 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -841,7 +841,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
FIXME: params et cstr_expr (arity) *)
let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
(rawlist:(Id.t * glob_constr) list) =
- let lident = Loc.ghost, shift.ident in
+ let lident = (Loc.ghost, shift.ident), None in
let bindlist , cstr_expr = (* params , arities *)
merge_rec_params_and_arity prms1 prms2 shift mkSet in
let lcstor_expr : (bool * (lident * constr_expr)) list =
@@ -884,10 +884,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,impls = Command.interp_mutual_inductive indl []
+ let mie,pl,impls = Command.interp_mutual_inductive indl []
false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
- ignore (Command.declare_mutual_inductive_with_eliminations mie impls)
+ ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
(* Find infos on identifier id. *)
@@ -902,7 +902,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
(** [merge id1 id2 args1 args2 id] builds and declares a new inductive
type called [id], representing the merged graphs of both graphs
- [ind1] and [ind2]. identifiers occuring in both arrays [args1] and
+ [ind1] and [ind2]. identifiers occurring in both arrays [args1] and
[args2] are considered linked (i.e. are the same variable) in the
new graph.
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0999b95d..5d41ec72 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -115,7 +115,7 @@ let pf_get_new_ids idl g =
let compute_renamed_type gls c =
rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
- (pf_type_of gls c)
+ (pf_unsafe_type_of gls c)
let h'_id = Id.of_string "h'"
let teq_id = Id.of_string "teq"
let ano_id = Id.of_string "anonymous"
@@ -194,7 +194,7 @@ let (value_f:constr list -> global_reference -> constr) =
Anonymous)],
GVar(d0,v_id)])
in
- let body = fst (understand env Evd.empty glob_body)(*FIXME*) in
+ let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
it_mkLambda_or_LetIn body context
let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
@@ -305,7 +305,8 @@ let check_not_nested forbidden e =
| Rel _ -> ()
| Var x ->
if Id.List.mem x forbidden
- then error ("check_not_nested : failure "^Id.to_string x)
+ then errorlabstrm "Recdef.check_not_nested"
+ (str "check_not_nested: failure " ++ pr_id x)
| Meta _ | Evar _ | Sort _ -> ()
| Cast(e,_,t) -> check_not_nested e;check_not_nested t
| Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -399,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
thin to_intros;
h_intros to_intros;
(fun g' ->
- let ty_teq = pf_type_of g' (mkVar heq) in
+ let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
let teq_lhs,teq_rhs =
let _,args = try destApp ty_teq with DestKO -> assert false in
args.(1),args.(2)
@@ -513,13 +514,13 @@ let rec prove_lt hyple g =
in
let h =
List.find (fun id ->
- match decompose_app (pf_type_of g (mkVar id)) with
+ match decompose_app (pf_unsafe_type_of g (mkVar id)) with
| _, t::_ -> eq_constr t varx
| _ -> false
) hyple
in
let y =
- List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
+ List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in
observe_tclTHENLIST (str "prove_lt1")[
Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
observe_tac (str "prove_lt") (prove_lt hyple)
@@ -654,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden}
let pf_type c tac gl =
- let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in
+ let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
let pf_typel l tac =
@@ -679,7 +680,7 @@ let mkDestructEq :
if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
then None else Some id) hyps in
let to_revert_constr = List.rev_map mkVar to_revert in
- let type_of_expr = pf_type_of g expr in
+ let type_of_expr = pf_unsafe_type_of g expr in
let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
to_revert_constr in
pf_typel new_hyps (fun _ ->
@@ -1292,8 +1293,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
ref_ := Some lemma ;
let lid = ref [] in
let h_num = ref (-1) in
+ let env = Global.env () in
Proof_global.discard_all ();
- build_proof Evd.empty
+ build_proof (Evd.from_env env)
( fun gls ->
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
observe_tclTHENLIST (str "")
@@ -1397,9 +1399,7 @@ let com_terminate
start_proof ctx tclIDTAC tclIDTAC;
try
let sigma, new_goal_type = build_new_goal_type () in
- let sigma =
- Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env
- in
+ let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in
open_new_goal start_proof sigma
using_lemmas tcc_lemma_ref
(Some tcc_lemma_name)
@@ -1436,9 +1436,7 @@ let (com_eqn : int -> Id.t ->
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
in
let (evmap, env) = Lemmas.get_current_context() in
- let evmap =
- Evd.from_env ~ctx:(Evd.evar_universe_context evmap) Environ.empty_env
- in
+ let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
@@ -1511,12 +1509,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let equation_id = add_suffix function_name "_equation" in
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
- let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in
+ let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in
let relation =
fst (*FIXME*)(interp_constr
env_with_pre_rec_args
- Evd.empty
+ (Evd.from_env env_with_pre_rec_args)
r)
in
let tcc_lemma_name = add_suffix function_name "_tcc" in
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 88c1a783..a36369d2 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -23,7 +23,7 @@ struct
- None , Some v -> \]-oo,v\]
- Some v, None -> \[v,+oo\[
- Some v, Some v' -> \[v,v'\]
- Intervals needs to be explicitely normalised.
+ Intervals needs to be explicitly normalised.
*)
type who = Left | Right
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 37428c39..aac9a7d3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -539,7 +539,7 @@ let context operation path (t : constr) =
in
loop 1 path t
-let occurence path (t : constr) =
+let occurrence path (t : constr) =
let rec loop p0 t = match (p0,kind_of_term t) with
| (p, Cast (c,_,_)) -> loop p c
| ([], _) -> t
@@ -555,7 +555,7 @@ let occurence path (t : constr) =
| ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
| ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
| (p, _) ->
- failwith ("occurence " ^ string_of_int(List.length p))
+ failwith ("occurrence " ^ string_of_int(List.length p))
in
loop path t
@@ -660,7 +660,7 @@ let clever_rewrite_gen_nat p result (t,args) =
let clever_rewrite p vpath t gl =
let full = pf_concl gl in
let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
- let vargs = List.map (fun p -> occurence p occ) vpath in
+ let vargs = List.map (fun p -> occurrence p occ) vpath in
let t' = applist(t, (vargs @ [abstracted])) in
exact (applist(t',[mkNewMeta()])) gl
@@ -1462,7 +1462,7 @@ let coq_omega =
let path = simplify_strong (new_id,new_var_num,display_var) system in
if !display_action_flag then display_action display_var path;
Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
- with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system"))
+ with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
end
end
@@ -1689,7 +1689,7 @@ let onClearedName2 id tac =
let destructure_hyps =
Proofview.Goal.nf_enter begin fun gl ->
- let type_of = Tacmach.New.pf_type_of gl in
+ let type_of = Tacmach.New.pf_unsafe_type_of gl in
let decidability = Tacmach.New.of_old decidability gl in
let pf_nf = Tacmach.New.of_old pf_nf gl in
let rec loop = function
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 8156e841..95407c5f 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -44,7 +44,7 @@ let occ_step_eq s1 s2 = match s1, s2 with
(* chemin identifiant une proposition sous forme du nom de l'hypothèse et
d'une liste de pas à partir de la racine de l'hypothèse *)
-type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
+type occurrence = {o_hyp : Names.Id.t; o_path : occ_path}
(* \subsection{refiable formulas} *)
type oformula =
@@ -81,7 +81,7 @@ and oequation = {
e_left: oformula; (* formule brute gauche *)
e_right: oformula; (* formule brute droite *)
e_trace: Term.constr; (* tactique de normalisation *)
- e_origin: occurence; (* l'hypothèse dont vient le terme *)
+ e_origin: occurrence; (* l'hypothèse dont vient le terme *)
e_negated: bool; (* vrai si apparait en position nié
après normalisation *)
e_depends: direction list; (* liste des points de disjonction dont
@@ -111,7 +111,7 @@ type environment = {
real_indices : (int,int) Hashtbl.t;
mutable cnt_connectors : int;
equations : (int,oequation) Hashtbl.t;
- constructors : (int, occurence) Hashtbl.t
+ constructors : (int, occurrence) Hashtbl.t
}
(* \subsection{Solution tree}
@@ -136,7 +136,7 @@ type solution_tree =
chemins pour extraire des equations ou d'hypothèses *)
type context_content =
- CCHyp of occurence
+ CCHyp of occurrence
| CCEqua of int
(* \section{Specific utility functions to handle base types} *)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2f9e8509..c7185ff2 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -155,14 +155,19 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
(****************************************************************************)
let ic c =
- let env = Global.env() and sigma = Evd.empty in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
Constrintern.interp_open_constr env sigma c
let ic_unsafe c = (*FIXME remove *)
- let env = Global.env() and sigma = Evd.empty in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
fst (Constrintern.interp_constr env sigma c)
-let ty c = Typing.type_of (Global.env()) Evd.empty c
+let ty c =
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
+ Typing.unsafe_type_of env sigma c
let decl_constant na ctx c =
let vars = Universes.universes_of_constr c in
@@ -215,7 +220,7 @@ let exec_tactic env evd n f args =
let gl = dummy_goal env evd in
let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in
let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
- Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd
+ Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd)
let stdlib_modules =
[["Coq";"Setoids";"Setoid"];