aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
authorPierre Courtieu2016-04-15 16:45:14 +0200
committerPierre Courtieu2016-04-15 16:45:14 +0200
commitcaa1f67de10614984fa7e1c68aa8adf0ff90196a (patch)
tree3c265ac5e16851c5dc1ca917ddb03725e09ea0ff /plugins/funind
parentbe824224cc76f729872e9d803fc64831b95aee94 (diff)
parent3b3d98acd58e91c960a2e11cd47ac19b2b34f86b (diff)
Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/functional_principles_proofs.ml90
-rw-r--r--plugins/funind/functional_principles_proofs.mli2
-rw-r--r--plugins/funind/functional_principles_types.ml97
-rw-r--r--plugins/funind/functional_principles_types.mli10
-rw-r--r--plugins/funind/g_indfun.ml4260
-rw-r--r--plugins/funind/glob_term_to_relation.ml151
-rw-r--r--plugins/funind/glob_termops.mli4
-rw-r--r--plugins/funind/indfun.ml92
-rw-r--r--plugins/funind/indfun_common.ml11
-rw-r--r--plugins/funind/indfun_common.mli6
-rw-r--r--plugins/funind/invfun.ml100
-rw-r--r--plugins/funind/merge.ml53
-rw-r--r--plugins/funind/recdef.ml89
14 files changed, 393 insertions, 574 deletions
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index a63941f0cb..e4433247b4 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 169a706005..02cd819f4a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -3,18 +3,19 @@ open Errors
open Util
open Term
open Vars
-open Context
open Namegen
open Names
open Declarations
open Pp
open Tacmach
+open Termops
open Proof_type
open Tacticals
open Tactics
open Indfun_common
open Libnames
open Globnames
+open Context.Rel.Declaration
(* let msgnl = Pp.msgnl *)
@@ -52,10 +53,10 @@ let rec print_debug_queue e =
let _ =
match e with
| Some e ->
- Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
| None ->
begin
- Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
end in
print_debug_queue None ;
end
@@ -229,7 +230,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
-let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
+let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
let nochange ?t' msg =
begin
observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
@@ -304,11 +305,11 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
in
let new_type_of_hyp,ctxt_size,witness_fun =
List.fold_left_i
- (fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
+ (fun i (end_of_type,ctxt_size,witness_fun) decl ->
try
let witness = Int.Map.find i sub in
- if not (Option.is_empty b') then anomaly (Pp.str "can not redefine a rel!");
- (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
+ if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
+ (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun))
with Not_found ->
(mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
)
@@ -371,12 +372,12 @@ let isLetIn t =
| _ -> false
-let h_reduce_with_zeta =
- reduce
+let h_reduce_with_zeta cl =
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
- })
+ }) cl)
@@ -536,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
(scan_type new_context new_t')
with Failure "NoChange" ->
(* Last thing todo : push the rel in the context and continue *)
- scan_type ((x,None,t_x)::context) t'
+ scan_type (LocalAssum (x,t_x) :: context) t'
end
end
else
@@ -705,9 +706,9 @@ let build_proof
in
tclTHENSEQ
[
- Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+ generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
thin dyn_infos.rec_hyps;
- pattern_option [Locus.AllOccurrencesBut [1],t] None;
+ Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
(fun g -> observe_tac "toto" (
tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
(fun g' ->
@@ -736,7 +737,8 @@ let build_proof
tclTHEN
(Proofview.V82.of_tactic intro)
(fun g' ->
- let (id,_,_) = pf_last_hyp g' in
+ let open Context.Named.Declaration in
+ let id = pf_last_hyp g' |> get_id in
let new_term =
pf_nf_betaiota g'
(mkApp(dyn_infos.info,[|mkVar id|]))
@@ -921,7 +923,9 @@ let generalize_non_dep hyp g =
let env = Global.env () 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) ->
+ let open Context.Named.Declaration in
+ Environ.fold_named_context_reverse (fun (clear,keep) decl ->
+ let hyp = get_id decl in
if Id.List.mem hyp hyps
|| List.exists (Termops.occur_var_in_decl env hyp) keep
|| Termops.occur_var env hyp hyp_typ
@@ -932,11 +936,11 @@ let generalize_non_dep hyp g =
in
(* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
tclTHEN
- ((* observe_tac "h_generalize" *) (Simple.generalize (List.map mkVar to_revert) ))
+ ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) ))
((* observe_tac "thin" *) (thin to_revert))
g
-let id_of_decl (na,_,_) = (Nameops.out_name na)
+let id_of_decl decl = Nameops.out_name (get_name decl)
let var_of_decl decl = mkVar (id_of_decl decl)
let revert idl =
tclTHEN
@@ -1044,7 +1048,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
(
fun g' ->
let just_introduced = nLastDecls nb_intro_to_do g' in
- let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
+ let open Context.Named.Declaration in
+ let just_introduced_id = List.map get_id just_introduced in
tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
(revert just_introduced_id) g'
)
@@ -1069,11 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(Name new_id)
)
in
- let fresh_decl =
- (fun (na,b,t) ->
- (fresh_id na,b,t)
- )
- in
+ let fresh_decl = map_name fresh_id in
let princ_info : elim_scheme =
{ princ_info with
params = List.map fresh_decl princ_info.params;
@@ -1120,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
)
in
observe (str "full_params := " ++
- prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+ prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
full_params
);
observe (str "princ_params := " ++
- prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+ prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
princ_params
);
observe (str "fbody_with_full_params := " ++
@@ -1165,7 +1166,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let pte_to_fix,rev_info =
List.fold_left_i
- (fun i (acc_map,acc_info) (pte,_,_) ->
+ (fun i (acc_map,acc_info) decl ->
+ let pte = get_name decl in
let infos = info_array.(i) in
let type_args,_ = decompose_prod infos.types in
let nargs = List.length type_args in
@@ -1259,7 +1261,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let args = nLastDecls nb_args g in
let fix_body = fix_info.body_with_param in
(* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
- let args_id = List.map (fun (id,_,_) -> id) args in
+ let open Context.Named.Declaration in
+ let args_id = List.map get_id args in
let dyn_infos =
{
nb_rec_hyps = -100;
@@ -1276,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(do_replace evd
full_params
(fix_info.idx + List.length princ_params)
- (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
+ (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params))
(all_funs.(fix_info.num_in_block))
fix_info.num_in_block
all_funs
@@ -1317,8 +1320,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
[
tclDO nb_args (Proofview.V82.of_tactic intro);
(fun g -> (* replacement of the function by its body *)
- let args = nLastDecls nb_args g in
- let args_id = List.map (fun (id,_,_) -> id) args in
+ let args = nLastDecls nb_args g in
+ let open Context.Named.Declaration in
+ let args_id = List.map get_id args in
let dyn_infos =
{
nb_rec_hyps = -100;
@@ -1334,7 +1338,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
tclTHENSEQ
- [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))];
+ [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]);
let do_prove =
build_proof
interactive_proof
@@ -1403,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
(* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *)
(* rewrite *)
(* ) *)
- Eauto.gen_eauto (false,5) [] (Some [])
+ Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some []))
]
gls
@@ -1460,7 +1464,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
(fun g ->
if is_mes
then
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g
else tclIDTAC g
);
observe_tac "rew_and_finish"
@@ -1472,7 +1476,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
tclCOMPLETE(
Eauto.eauto_with_bases
(true,5)
- [Evd.empty,Lazy.force refl_equal]
+ [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
[Hints.Hint_db.empty empty_transparent_state false]
)
)
@@ -1520,7 +1524,7 @@ let prove_principle_for_gen
avoid := new_id :: !avoid;
Name new_id
in
- let fresh_decl (na,b,t) = (fresh_id na,b,t) in
+ let fresh_decl = map_name fresh_id in
let princ_info : elim_scheme =
{ princ_info with
params = List.map fresh_decl princ_info.params;
@@ -1550,11 +1554,11 @@ let prove_principle_for_gen
in
let rec_arg_id =
match List.rev post_rec_arg with
- | (Name id,_,_)::_ -> id
+ | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id
| _ -> assert false
in
(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
- let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
+ let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in
let relation = substl subst_constrs relation in
let input_type = substl subst_constrs rec_arg_type in
let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
@@ -1562,7 +1566,7 @@ let prove_principle_for_gen
Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
in
let revert l =
- tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l)
+ tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
in
let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
@@ -1582,7 +1586,7 @@ let prove_principle_for_gen
)
g
in
- let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
+ let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in
let lemma =
match !tcc_lemma_ref with
| None -> error "No tcc proof !!"
@@ -1629,7 +1633,7 @@ let prove_principle_for_gen
[
observe_tac "start_tac" start_tac;
h_intros
- (List.rev_map (fun (na,_,_) -> Nameops.out_name na)
+ (List.rev_map (fun decl -> Nameops.out_name (get_name decl))
(princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
);
(* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1667,7 +1671,7 @@ let prove_principle_for_gen
in
let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in
let predicates_names =
- List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
+ List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates
in
let pte_info =
{ proving_tac =
@@ -1683,7 +1687,7 @@ let prove_principle_for_gen
is_mes acc_inv fix_id
(!tcc_list@(List.map
- (fun (na,_,_) -> (Nameops.out_name na))
+ (fun decl -> (Nameops.out_name (get_name decl)))
(princ_info.args@princ_info.params)
)@ ([acc_rec_arg_id])) eqs
)
@@ -1712,7 +1716,7 @@ let prove_principle_for_gen
(* observe_tac "instanciate_hyps_with_args" *)
(instanciate_hyps_with_args
make_proof
- (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
+ (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches)
(List.rev args_ids)
)
gl'
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 61fce267a3..34ce669672 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -8,7 +8,7 @@ val prove_princ_for_struct :
val prove_principle_for_gen :
- constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *)
+ constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
constr option ref -> (* a pointer to the obligation proofs lemma *)
bool -> (* is that function uses measure *)
int -> (* the number of recursive argument *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3edc590ccc..91a826c731 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -3,15 +3,16 @@ open Errors
open Util
open Term
open Vars
-open Context
open Namegen
open Names
open Pp
open Entries
open Tactics
+open Context.Rel.Declaration
open Indfun_common
open Functional_principles_proofs
open Misctypes
+open Sigma.Notations
exception Toberemoved_with_rel of int*constr
exception Toberemoved
@@ -29,14 +30,16 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let env = Global.env () in
let env_with_params = Environ.push_rel_context princ_type_info.params env in
let tbl = Hashtbl.create 792 in
- let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context) : rel_context =
+ let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t =
match predicates with
| [] -> []
- |(Name x,v,t)::predicates ->
- let id = Namegen.next_ident_away x avoid in
- Hashtbl.add tbl id x;
- (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
- | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ")
+ | decl :: predicates ->
+ (match Context.Rel.Declaration.get_name decl with
+ | Name x ->
+ let id = Namegen.next_ident_away x avoid in
+ Hashtbl.add tbl id x;
+ set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
+ | Anonymous -> anomaly (Pp.str "Anonymous property binder "))
in
let avoid = (Termops.ids_of_context env_with_params ) in
let princ_type_info =
@@ -46,15 +49,16 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
(* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
(* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
- let change_predicate_sort i (x,_,t) =
+ let change_predicate_sort i decl =
let new_sort = sorts.(i) in
- let args,_ = decompose_prod t in
+ let args,_ = decompose_prod (get_type decl) in
let real_args =
if princ_type_info.indarg_in_concl
then List.tl args
else args
in
- Nameops.out_name x,None,compose_prod real_args (mkSort new_sort)
+ Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
+ compose_prod real_args (mkSort new_sort))
in
let new_predicates =
List.map_i
@@ -69,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| _ -> error "Not a valid predicate"
)
in
- let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
+ let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in
let is_pte =
let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
fun t ->
@@ -114,7 +118,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| Rel n ->
begin
try match Environ.lookup_rel n env with
- | _,_,t when is_dom t -> raise Toberemoved
+ | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved
| _ -> pre_princ,[]
with Not_found -> assert false
end
@@ -159,7 +163,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
try
let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
let new_x : Name.t = get_name (Termops.ids_of_context env) x in
- let new_env = Environ.push_rel (x,None,t) env in
+ let new_env = Environ.push_rel (LocalAssum (x,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
@@ -188,7 +192,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
let new_x : Name.t = get_name (Termops.ids_of_context env) x in
- let new_env = Environ.push_rel (x,Some v,t) env in
+ let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
@@ -227,7 +231,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
it_mkProd_or_LetIn
(it_mkProd_or_LetIn
- pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b)
+ pre_res (List.map (function Context.Named.Declaration.LocalAssum (id,b) -> LocalAssum (Name (Hashtbl.find tbl id), b)
+ | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b))
new_predicates)
)
princ_type_info.params
@@ -235,10 +240,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let change_property_sort evd toSort princ princName =
+ let open Context.Rel.Declaration in
let princ_info = compute_elim_sig princ in
- let change_sort_in_predicate (x,v,t) =
- (x,None,
- let args,ty = decompose_prod t in
+ let change_sort_in_predicate decl =
+ LocalAssum
+ (get_name decl,
+ let args,ty = decompose_prod (get_type decl) in
let s = destSort ty in
Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
compose_prod args (mkSort toSort)
@@ -291,7 +298,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* let dur1 = System.time_difference tim1 tim2 in *)
(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
(* end; *)
- get_proof_clean true, Ephemeron.create hook
+ get_proof_clean true, CEphemeron.create hook
end
@@ -303,7 +310,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 +325,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.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 +402,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 +454,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
@@ -483,11 +491,10 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
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 +548,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,19 +592,17 @@ 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 =
@@ -622,18 +627,15 @@ 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 *)
@@ -653,12 +655,15 @@ let build_case_scheme fa =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
in
- let ind_fun =
+ let (ind, sf) =
let ind = first_fun_kn,funs_indexes in
(ind,Univ.Instance.empty)(*FIXME*),prop_sort
in
- let sigma, scheme =
- (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma (scheme, sigma, _) =
+ Indrec.build_case_analysis_scheme_default env sigma ind sf
+ in
+ let sigma = Sigma.to_evar_map sigma in
let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in
let sorts =
(fun (_,_,x) ->
@@ -673,14 +678,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 f6e5578d2e..3fa2644ca9 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-2016 *)
+(* \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 61f03d6f22..e93c395e3d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -16,8 +16,12 @@ open Constrexpr
open Indfun_common
open Indfun
open Genarg
+open Constrarg
open Tacticals
open Misctypes
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
DECLARE PLUGIN "recdef_plugin"
@@ -55,7 +59,9 @@ let pr_with_bindings_typed prc prlc (c,bl) =
let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
- | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it)
+ | Some b ->
+ let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
+ spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
ARGUMENT EXTEND fun_ind_using
@@ -88,7 +94,7 @@ let out_disjunctive = function
| loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
| _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
-ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat
+ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
| [] ->[ None ]
END
@@ -144,10 +150,10 @@ module Tactic = Pcoq.Tactic
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
- Genarg.create_arg None "function_rec_definition_loc"
+ Genarg.create_arg "function_rec_definition_loc"
let function_rec_definition_loc =
- Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+ Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
GEXTEND Gram
GLOBAL: function_rec_definition_loc ;
@@ -247,247 +253,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_unsafe_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_unsafe_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.unsafe_type_of (Global.env()) Evd.empty f1 in
- let f2type = Typing.unsafe_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 065c12a2d7..8a0a1a064d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,33 +333,36 @@ 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
- Environ.push_named (id,value,typ) env
+ 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
+ let open Context.Named.Declaration in
+ Environ.push_named (of_tuple (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);
+ let open Context.Rel.Declaration in
+ 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
+ | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,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
let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
- let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
+ let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
in
let new_env = add_pat_variables env pat typ in
let res =
fst (
- Context.fold_rel_context
- (fun (na,v,t) (env,ctxt) ->
- match na with
+ Context.Rel.fold_outside
+ (fun decl (env,ctxt) ->
+ let _,v,t = Context.Rel.Declaration.to_tuple decl in
+ match Context.Rel.Declaration.get_name decl with
| Anonymous -> assert false
| Name id ->
let new_t = substl ctxt t in
@@ -370,13 +373,14 @@ let add_pat_variables pat typ env : Environ.env =
Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
);
- (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
+ let open Context.Named.Declaration in
+ (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt)
)
(Environ.rel_context new_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,19 +397,20 @@ 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
let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
- let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
+ let open Context.Rel.Declaration in
+ let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
let _,cstl = Inductiveops.dest_ind_family indf in
let csta = Array.of_list cstl in
let implicit_args =
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 +491,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.unsafe_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,12 +599,13 @@ 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.unsafe_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 =
+ let open Context.Named.Declaration in
match n with
Anonymous -> env
- | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env
+ | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env
in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_letin n) v_res b_res
@@ -610,10 +616,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.unsafe_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 +648,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.unsafe_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 " ++
@@ -681,7 +687,7 @@ and build_entry_lc_from_case env funname make_discr
let case_resl =
List.fold_right
(fun (case_arg,_) ctxt_argsl ->
- let arg_res = build_entry_lc env funname avoid case_arg in
+ let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in
combine_results combine_args arg_res ctxt_argsl
)
el
@@ -689,8 +695,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.unsafe_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 +743,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.unsafe_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 +791,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.unsafe_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
@@ -875,7 +881,7 @@ exception Continue
*)
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
observe (str "rebuilding : " ++ pr_glob_constr rt);
-
+ let open Context.Rel.Declaration in
match rt with
| GProd(_,n,k,t,b) ->
let not_free_in_t id = not (is_free_in id t) in
@@ -894,8 +900,8 @@ 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 new_env = Environ.push_rel (n,None,t') env in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
+ let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -914,7 +920,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
@@ -926,7 +932,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let subst_b =
if is_in_b then b else replace_var_by_term id rt b
in
- let new_env = Environ.push_rel (n,None,t') env in
+ let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons
new_env
@@ -937,7 +943,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 +955,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 +965,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
@@ -970,20 +976,19 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(fun acc var_as_constr arg ->
if isRel var_as_constr
then
- let (na,_,_) =
- Environ.lookup_rel (destRel var_as_constr) env
- in
+ let open Context.Rel.Declaration in
+ let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in
match na with
| Anonymous -> acc
| 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,8 +1014,8 @@ 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
- Environ.push_rel (n,None,t') env
+ let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
+ Environ.push_rel (LocalAssum (n,t')) env
in
let new_b,id_to_exclude =
rebuild_cons
@@ -1047,8 +1052,8 @@ 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 new_env = Environ.push_rel (n,None,t') env in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
+ let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1063,8 +1068,8 @@ 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 new_env = Environ.push_rel (n,None,t') env in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) t in
+ let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1082,10 +1087,10 @@ 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
+ let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1104,9 +1109,11 @@ 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.unsafe_type_of env Evd.empty t' in
- let new_env = Environ.push_rel (n,Some t',type_t') env 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 (LocalDef (n,t',type_t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1129,8 +1136,8 @@ 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 new_env = Environ.push_rel (na,None,t') env in
+ let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
+ let new_env = Environ.push_rel (LocalAssum (na,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1252,12 +1259,13 @@ let do_build_inductive
let relnames = Array.map mk_rel_id funnames in
let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
(* Construction of the pseudo constructors *)
+ let open Context.Named.Declaration in
let evd,env =
Array.fold_right2
(fun id c (evd,env) ->
let evd,t = Typing.type_of env evd (mkConstU c) in
evd,
- Environ.push_named (id,None,t)
+ Environ.push_named (LocalAssum (id,t))
(* try *)
(* Typing.e_type_of env evd (mkConstU c) *)
(* with Not_found -> *)
@@ -1296,8 +1304,8 @@ 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
+ Environ.push_named (LocalAssum (rel_name,
+ 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 +1403,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 +1468,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 0f10636f0f..179e8fe8d9 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 5dcb0c0439..84a4d910ef 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,3 +1,4 @@
+open Context.Rel.Declaration
open Errors
open Util
open Names
@@ -10,12 +11,13 @@ open Glob_term
open Declarations
open Misctypes
open Decl_kinds
+open Sigma.Notations
let is_rec_info scheme_info =
- let test_branche min acc (_,_,br) =
+ let test_branche min acc decl =
acc || (
let new_branche =
- it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in
+ it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in
let free_rels_in_br = Termops.free_rels new_branche in
let max = min + scheme_info.Tactics.npredicates in
Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
@@ -27,7 +29,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 ->
@@ -86,7 +87,7 @@ let functional_induction with_clean c princl pat =
in
let encoded_pat_as_patlist =
List.make (List.length args + List.length c_list - 1) None @ [pat] in
- List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None))
+ List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
(args@c_list) encoded_pat_as_patlist
in
let princ' = Some (princ,bindings) in
@@ -113,7 +114,7 @@ let functional_induction with_clean c princl pat =
in
Tacticals.tclTHEN
(Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
- (Tactics.reduce flag Locusops.allHypsAndConcl)
+ (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl))
g
else Tacticals.tclIDTAC g
in
@@ -123,9 +124,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,18 +144,18 @@ 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))
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
(env0,Constrintern.empty_internalization_env) lnameargsardef in
let recdef =
(* Declare local notations *)
@@ -228,7 +227,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 +322,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 +342,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 +354,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 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 (Global.env ()) evd uprinc 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 +381,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 +403,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 +595,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 +615,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 +626,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 +639,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 +650,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 +673,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 +681,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
@@ -729,9 +730,9 @@ let rec add_args id new_args b =
List.map (fun (e,o) -> add_args id new_args e,o) bl)
| CCases(loc,sty,b_option,cel,cal) ->
CCases(loc,sty,Option.map (add_args id new_args) b_option,
- List.map (fun (b,(na,b_option)) ->
+ List.map (fun (b,na,b_option) ->
add_args id new_args b,
- (na, b_option)) cel,
+ na, b_option) cel,
List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
)
| CLetTuple(loc,nal,(na,b_option),b1,b2) ->
@@ -753,10 +754,8 @@ let rec add_args id new_args b =
| CCast(loc,b1,b2) ->
CCast(loc,add_args id new_args b1,
Miscops.map_cast_type (add_args id new_args) b2)
- | CRecord (loc, w, pars) ->
- CRecord (loc,
- (match w with Some w -> Some (add_args id new_args w) | _ -> None),
- List.map (fun (e,o) -> e, add_args id new_args o) pars)
+ | CRecord (loc, pars) ->
+ CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars)
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
| CPrim _ -> b
@@ -830,15 +829,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 +866,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 1c409500ef..2449678a13 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -149,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
@@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook =
(locality, ConstRef kn)
in
if with_clean then Pfedit.delete_current_proof ();
- Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
+ CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
definition_message id
@@ -180,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;
@@ -195,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
@@ -203,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 10daf6e848..e5c756f564 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,15 +46,15 @@ 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 ->
- unit Lemmas.declaration_hook Ephemeron.key -> unit
+val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind ->
+ unit Lemmas.declaration_hook CEphemeron.key -> unit
(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
abort the proof
*)
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 89ceb751a4..6a5a5ad533 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,10 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+
open Tacexpr
open Declarations
open Errors
@@ -19,6 +20,8 @@ open Tactics
open Indfun_common
open Tacmach
open Misctypes
+open Termops
+open Context.Rel.Declaration
(* Some pretty printing function for debugging purpose *)
@@ -70,8 +73,8 @@ let do_observe_tac s tac g =
with reraise ->
let reraise = Errors.push reraise in
let e = Cerrors.process_vernac_interp_error reraise in
- observe (str "observation "++ s++str " raised exception " ++
- Errors.iprint e ++ str " on goal " ++ goal );
+ observe (hov 0 (str "observation "++ s++str " raised exception " ++
+ Errors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
iraise reraise;;
@@ -133,18 +136,21 @@ let generate_type evd g_to_f f graph i =
let fun_ctxt,res_type =
match ctxt with
| [] | [_] -> anomaly (Pp.str "Not a valid context")
- | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
+ | decl :: fun_ctxt -> fun_ctxt, get_type decl
in
let rec args_from_decl i accu = function
| [] -> accu
- | (_, Some _, _) :: l ->
+ | LocalDef _ :: l ->
args_from_decl (succ i) accu l
| _ :: l ->
let t = mkRel i in
args_from_decl (succ i) (t :: accu) l
in
(*i We need to name the vars [res] and [fv] i*)
- let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
+ let filter = fun decl -> match get_name decl with
+ | Name id -> Some id
+ | Anonymous -> None
+ in
let named_ctxt = List.map_filter filter fun_ctxt in
let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in
@@ -170,12 +176,12 @@ let generate_type evd g_to_f f graph i =
\[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \]
i*)
let pre_ctxt =
- (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(f,args_as_rels)),res_type)::fun_ctxt
+ LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
in
(*i and we can return the solution depending on which lemma type we are defining i*)
if g_to_f
- then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
- else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+ then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+ else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
(*
@@ -259,10 +265,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(* and built the intro pattern for each of them *)
let intro_pats =
List.map
- (fun (_,_,br_type) ->
+ (fun decl ->
List.map
(fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
- (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+ (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl)))))
)
branches
in
@@ -362,14 +368,14 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(* unfolding of all the defined variables introduced by this branch *)
(* observe_tac "unfolding" pre_tac; *)
(* $zeta$ normalizing of the conclusion *)
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{ Redops.all_flags with
Genredexpr.rDelta = false ;
Genredexpr.rConst = []
}
)
- Locusops.onConcl;
+ Locusops.onConcl);
observe_tac ("toto ") tclIDTAC;
(* introducing the the result of the graph and the equality hypothesis *)
@@ -389,10 +395,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(fun ((_,(ctxt,concl))) ->
match ctxt with
| [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
- | hres::res::(x,_,t)::ctxt ->
+ | hres::res::decl::ctxt ->
let res = Termops.it_mkLambda_or_LetIn
(Termops.it_mkProd_or_LetIn concl [hres;res])
- ((x,None,t)::ctxt)
+ (LocalAssum (get_name decl, get_type decl) :: ctxt)
in
res
)
@@ -407,8 +413,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let bindings =
let params_bindings,avoid =
List.fold_left2
- (fun (bindings,avoid) (x,_,_) p ->
- let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
+ (fun (bindings,avoid) decl p ->
+ let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
p::bindings,id::avoid
)
([],pf_ids_of_hyps g)
@@ -417,8 +423,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
in
let lemmas_bindings =
List.rev (fst (List.fold_left2
- (fun (bindings,avoid) (x,_,_) p ->
- let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
+ (fun (bindings,avoid) decl p ->
+ let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
(nf_zeta p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
@@ -454,10 +460,11 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
generalize every hypothesis which depends of [x] but [hyp]
*)
let generalize_dependent_of x hyp g =
+ let open Context.Named.Declaration in
tclMAP
(function
- | (id,None,t) when not (Id.equal id hyp) &&
- (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id])
+ | LocalAssum (id,t) when not (Id.equal id hyp) &&
+ (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id])
| _ -> tclIDTAC
)
(pf_hyps g)
@@ -467,6 +474,15 @@ let generalize_dependent_of x hyp g =
(* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
(unfolding, substituting, destructing cases \ldots)
*)
+let tauto =
+ let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
+ let mp = ModPath.MPfile (DirPath.make dp) in
+ let kn = KerName.make2 mp (Label.make "tauto") in
+ Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
+ let body = Tacenv.interp_ltac kn in
+ Tacinterp.eval_tactic body
+ end
+
let rec intros_with_rewrite g =
observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
and intros_with_rewrite_aux : tactic =
@@ -483,15 +499,15 @@ and intros_with_rewrite_aux : tactic =
tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g))
then tclTHENSEQ[
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))];
- tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]);
+ tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )))
(pf_ids_of_hyps g);
intros_with_rewrite
] g
else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g))
then tclTHENSEQ[
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))];
- tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]);
+ tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )))
(pf_ids_of_hyps g);
intros_with_rewrite
] g
@@ -523,7 +539,7 @@ and intros_with_rewrite_aux : tactic =
] g
end
| Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
- Proofview.V82.of_tactic Tauto.tauto g
+ Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENSEQ[
Proofview.V82.of_tactic (simplest_case v);
@@ -531,12 +547,12 @@ and intros_with_rewrite_aux : tactic =
] g
| LetIn _ ->
tclTHENSEQ[
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
})
- Locusops.onConcl
+ Locusops.onConcl)
;
intros_with_rewrite
] g
@@ -546,12 +562,12 @@ and intros_with_rewrite_aux : tactic =
end
| LetIn _ ->
tclTHENSEQ[
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
})
- Locusops.onConcl
+ Locusops.onConcl)
;
intros_with_rewrite
] g
@@ -662,10 +678,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
let branches = List.rev princ_infos.branches in
let intro_pats =
List.map
- (fun (_,_,br_type) ->
+ (fun decl ->
List.map
(fun id -> id)
- (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type))
+ (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl)))
)
branches
in
@@ -691,18 +707,18 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
(* Don't forget to $\zeta$ normlize the term since the principles
have been $\zeta$-normalized *)
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
})
- Locusops.onConcl
+ Locusops.onConcl)
;
- Simple.generalize (List.map mkVar ids);
+ generalize (List.map mkVar ids);
thin ids
]
else
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))])
in
(* The proof of each branche itself *)
let ind_number = ref 0 in
@@ -737,7 +753,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
tclTHENSEQ
[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
observe_tac "h_generalize"
- (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+ (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
Proofview.V82.of_tactic (Simple.intro graph_principle_id);
observe_tac "" (tclTHEN_i
(observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
@@ -760,7 +776,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
@@ -829,7 +846,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 +891,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
@@ -920,7 +936,7 @@ let revert_graph kn post_tac hid g =
let f_args,res = Array.chop (Array.length args - 1) args in
tclTHENSEQ
[
- Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+ generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
post_tac hid
@@ -964,7 +980,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
in
tclTHENSEQ[
pre_tac hid;
- Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+ generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ea699580b9..c71d9a9ca4 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -19,12 +19,12 @@ open Pp
open Names
open Term
open Vars
-open Context
open Termops
open Declarations
open Glob_term
open Glob_termops
open Decl_kinds
+open Context.Rel.Declaration
(** {1 Utilities} *)
@@ -135,9 +135,9 @@ let showind (id:Id.t) =
let cstrid = Constrintern.global_reference id in
let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
- List.iter (fun (nm, optcstr, tp) ->
- print_string (string_of_name nm^":");
- prconstr tp; print_string "\n")
+ List.iter (fun decl ->
+ print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
+ prconstr (get_type decl); print_string "\n")
ib1.mind_arity_ctxt;
Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1);
Array.iteri
@@ -258,27 +258,27 @@ type merge_infos =
lnk2: int merged_arg array;
(** rec params which remain rec param (ie not linked) *)
- recprms1: rel_declaration list;
- recprms2: rel_declaration list;
+ recprms1: Context.Rel.Declaration.t list;
+ recprms2: Context.Rel.Declaration.t list;
nrecprms1: int;
nrecprms2: int;
(** rec parms which became non parm (either linked to something
or because after a rec parm that became non parm) *)
- otherprms1: rel_declaration list;
- otherprms2: rel_declaration list;
+ otherprms1: Context.Rel.Declaration.t list;
+ otherprms2: Context.Rel.Declaration.t list;
notherprms1:int;
notherprms2:int;
(** args which remain args in merge *)
- args1:rel_declaration list;
- args2:rel_declaration list;
+ args1:Context.Rel.Declaration.t list;
+ args2:Context.Rel.Declaration.t list;
nargs1:int;
nargs2:int;
(** functional result args *)
- funresprms1: rel_declaration list;
- funresprms2: rel_declaration list;
+ funresprms1: Context.Rel.Declaration.t list;
+ funresprms2: Context.Rel.Declaration.t list;
nfunresprms1:int;
nfunresprms2:int;
}
@@ -460,11 +460,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
let _ = prstr "\notherprms1:\n" in
let _ =
- List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+ List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : ");
+ prconstr (get_type decl); prstr "\n")
otherprms1 in
let _ = prstr "\notherprms2:\n" in
let _ =
- List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+ List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n")
otherprms2 in
{
ident=id;
@@ -824,9 +825,11 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
let arity,_ =
List.fold_left
- (fun (acc,env) (nm,_,c) ->
+ (fun (acc,env) decl ->
+ let nm = Context.Rel.Declaration.get_name decl in
+ let c = get_type decl in
let typ = Constrextern.extern_constr false env Evd.empty c in
- let newenv = Environ.push_rel (nm,None,c) env in
+ let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
(concl,Global.env())
(shift.funresprms2 @ shift.funresprms1
@@ -841,7 +844,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 =
@@ -851,12 +854,12 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
lident , bindlist , Some cstr_expr , lcstor_expr
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
+let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
match rdecl with
- | (nme,None,t) ->
+ | LocalAssum (nme,t) ->
let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
GProd (Loc.ghost,nme,Explicit,traw,t2)
- | (_,Some _,_) -> assert false
+ | LocalDef _ -> assert false
(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
@@ -884,10 +887,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 +905,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.
@@ -970,7 +973,7 @@ let funify_branches relinfo nfuns branch =
| Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
| _ -> false in
(* FIXME: *)
- (Anonymous,Some mkProp,mkProp)
+ LocalDef (Anonymous,mkProp,mkProp)
let relprinctype_to_funprinctype relprinctype nfuns =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b5a42b3078..046c7aa437 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -29,6 +29,7 @@ open Proof_type
open Pfedit
open Glob_term
open Pretyping
+open Termops
open Constrintern
open Misctypes
open Genredexpr
@@ -38,7 +39,8 @@ open Auto
open Eauto
open Indfun_common
-
+open Sigma.Notations
+open Context.Rel.Declaration
(* Ugly things which should not be here *)
@@ -179,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) =
)
in
let context = List.map
- (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al))
+ (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al))
in
let env = Environ.push_rel_context context (Global.env ()) in
let glob_body =
@@ -194,7 +196,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) =
@@ -203,7 +205,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob
-(* Debuging mechanism *)
+(* Debugging mechanism *)
let debug_queue = Stack.create ()
let rec print_debug_queue b e =
@@ -212,10 +214,10 @@ let rec print_debug_queue b e =
begin
let lmsg,goal = Stack.pop debug_queue in
if b then
- Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
else
begin
- Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
end;
(* print_debug_queue false e; *)
end
@@ -274,8 +276,8 @@ let tclUSER tac is_mes l g =
if is_mes
then observe_tclTHENLIST (str "tclUSER2")
[
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
- (delayed_force Indfun_common.ltof_ref))];
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
+ (delayed_force Indfun_common.ltof_ref))]);
tac
]
else tac
@@ -291,9 +293,9 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
-(* Travelling term.
+(* Traveling term.
Both definitions of [f_terminate] and [f_equation] use the same generic
- travelling mechanism.
+ traveling mechanism.
*)
(* [check_not_nested forbidden e] checks that [e] does not contains any variable
@@ -327,7 +329,7 @@ let check_not_nested forbidden e =
with UserError(_,p) ->
errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
-(* ['a info] contains the local information for travelling *)
+(* ['a info] contains the local information for traveling *)
type 'a infos =
{ nb_arg : int; (* function number of arguments *)
concl_tac : tactic; (* final tactic to finish proofs *)
@@ -337,7 +339,7 @@ type 'a infos =
f_id : Id.t; (* function name *)
f_constr : constr; (* function term *)
f_terminate : constr; (* termination proof term *)
- func : global_reference; (* functionnal reference *)
+ func : global_reference; (* functional reference *)
info : 'a;
is_main_branch : bool; (* on the main branch or on a matched expression *)
is_final : bool; (* final first order term or not *)
@@ -357,7 +359,7 @@ type ('a,'b) journey_info_tac =
'b infos -> (* argument of the tactic *)
tactic
-(* journey_info : specifies the actions to do on the different term constructors during the travelling of the term
+(* journey_info : specifies the actions to do on the different term constructors during the traveling of the term
*)
type journey_info =
{ letiN : ((Name.t*constr*types*constr),constr) journey_info_tac;
@@ -560,10 +562,10 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
observe_tclTHENLIST (str "destruct_bounds_aux2")[
observe_tac (str "clearing k ") (clear [id]);
h_intros [k;h';def];
- observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl);
+ observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
observe_tac (str "unfold functional")
- (unfold_in_concl[(Locus.OnlyOccurrences [1],
- evaluable_of_global_reference infos.func)]);
+ (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+ evaluable_of_global_reference infos.func)]));
(
observe_tclTHENLIST (str "test")[
list_rewrite true
@@ -676,8 +678,10 @@ let mkDestructEq :
let hyps = pf_hyps g in
let to_revert =
Util.List.map_filter
- (fun (id, _, t) ->
- if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
+ (fun decl ->
+ let open Context.Named.Declaration in
+ let id = get_id decl in
+ if Id.List.mem id not_on_hyp || not (Termops.occur_term expr (get_type decl))
then None else Some id) hyps in
let to_revert_constr = List.rev_map mkVar to_revert in
let type_of_expr = pf_unsafe_type_of g expr in
@@ -685,11 +689,13 @@ let mkDestructEq :
to_revert_constr in
pf_typel new_hyps (fun _ ->
observe_tclTHENLIST (str "mkDestructEq")
- [Simple.generalize new_hyps;
+ [generalize new_hyps;
(fun g2 ->
- Proofview.V82.of_tactic (change_in_concl None
- (fun patvars sigma ->
- pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2);
+ let changefun patvars = { run = fun sigma ->
+ let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
+ redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
+ } in
+ Proofview.V82.of_tactic (change_in_concl None changefun) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -897,10 +903,10 @@ let make_rewrite expr_info l hp max =
[observe_tac(str "make_rewrite finalize") (
(* tclORELSE( h_reflexivity) *)
(observe_tclTHENLIST (str "make_rewrite")[
- simpl_iter Locusops.onConcl;
+ Proofview.V82.of_tactic (simpl_iter Locusops.onConcl);
observe_tac (str "unfold functional")
- (unfold_in_concl[(Locus.OnlyOccurrences [1],
- evaluable_of_global_reference expr_info.func)]);
+ (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+ evaluable_of_global_reference expr_info.func)]));
(list_rewrite true
(List.map (fun e -> mkVar e,true) expr_info.eqs));
@@ -1110,7 +1116,7 @@ let termination_proof_header is_mes input_type ids args_id relation
[observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
- tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id]))
+ tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))
))
;
observe_tac (str "fix") (fix (Some hrec) (nargs+1));
@@ -1248,7 +1254,7 @@ let clear_goals =
then Termops.pop b'
else if b' == b then t
else mkProd(na,t',b')
- | _ -> map_constr clear_goal t
+ | _ -> Term.map_constr clear_goal t
in
List.map clear_goal
@@ -1293,13 +1299,14 @@ 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 "")
[
- Simple.generalize [lemma];
+ generalize [lemma];
Proofview.V82.of_tactic (Simple.intro hid);
(fun g ->
let ids = pf_ids_of_hyps g in
@@ -1329,7 +1336,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
(Proofview.V82.of_tactic e_assumption);
Eauto.eauto_with_bases
(true,5)
- [Evd.empty,Lazy.force refl_equal]
+ [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
[Hints.Hint_db.empty empty_transparent_state false]
]
)
@@ -1398,9 +1405,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)
@@ -1421,7 +1426,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let x = n_x_id ids nargs in
observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
h_intros x;
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
observe_tac (str "simplest_case")
(Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
Array.of_list (List.map mkVar x)))));
@@ -1437,9 +1442,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)
@@ -1487,7 +1490,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let env = Global.env() in
let evd = ref (Evd.from_env env) in
let function_type = interp_type_evars env evd type_of_f in
- let env = push_named (function_name,None,function_type) env in
+ let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
let ty = interp_type_evars env evd ~impls:rec_impls eq in
let evm, nf = Evarutil.nf_evars_and_universes !evd in
@@ -1495,7 +1498,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let function_type = nf function_type in
(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
let res_vars,eq' = decompose_prod equation_lemma_type in
- let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
+ let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
let eq' = nf_zeta env_eq' eq' in
let res =
(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
@@ -1512,12 +1515,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 env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env 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) -> LocalAssum (x,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:14:38 +0000