diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/FunInd.v | 10 | ||||
| -rw-r--r-- | plugins/funind/Recdef.v | 10 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.mli | 10 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 17 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 75 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 20 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 111 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 9 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 14 | ||||
| -rw-r--r-- | plugins/funind/invfun.mli | 10 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 33 |
12 files changed, 167 insertions, 154 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v index b8a05e5cc0..12458c1072 100644 --- a/plugins/funind/FunInd.v +++ b/plugins/funind/FunInd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Coq.extraction.Extraction. diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index 8b4dbbb45c..d94e62b45a 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export Coq.funind.FunInd. diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index ad396a2cbb..33aeafef81 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 4b828a7022..90af20b4ca 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -1,11 +1,12 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Util open Pp @@ -67,9 +68,9 @@ let pr_intro_as_pat _prc _ _ pat = str"<simple_intropattern>" | None -> mt () -let out_disjunctive = function - | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.") +let out_disjunctive = CAst.map (function + | IntroAction (IntroOrAndPattern l) -> l + | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")) ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f7639d22d6..49f7aae435 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -287,7 +287,7 @@ let make_discr_match_el = *) let make_discr_match_brl i = List.map_i - (fun j (_,(idl,patl,_)) -> Loc.tag @@ + (fun j {CAst.v=(idl,patl,_)} -> CAst.make @@ if Int.equal j i then (idl,patl, mkGRef (Lazy.force coq_True_ref)) else (idl,patl, mkGRef (Lazy.force coq_False_ref)) @@ -352,9 +352,9 @@ let raw_push_named (na,raw_value,raw_typ) env = let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in (match raw_value with | None -> - Environ.push_named (NamedDecl.LocalAssum (id,typ)) env + EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env | Some value -> - Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env) + EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env) let add_pat_variables pat typ env : Environ.env = @@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = The "value" of this branch is then simply [res] *) 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) (EConstr.of_constr rt_as_constr) in + let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty 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 @@ -631,12 +631,11 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v 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) (EConstr.of_constr v_as_constr) in - let v_type = EConstr.Unsafe.to_constr v_type in + let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = match n with Anonymous -> env - | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env + | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,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 @@ -648,7 +647,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = 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.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) 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.from_env env) b_typ with Not_found -> @@ -660,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = assert (Int.equal (Array.length case_pats) 2); let brl = List.map_i - (fun i x -> Loc.tag ([],[case_pats.(i)],x)) + (fun i x -> CAst.make ([],[case_pats.(i)],x)) 0 [lhs;rhs] in @@ -680,7 +679,7 @@ 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.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) 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.from_env env) b_typ with Not_found -> @@ -690,7 +689,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); - let br = Loc.tag ([],[case_pats.(0)],e) in + let br = CAst.make ([],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr @@ -726,7 +725,7 @@ and build_entry_lc_from_case env funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in - EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr)) + EConstr.Unsafe.to_constr (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 ****) @@ -757,7 +756,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve | [] -> (* computed_branches *) {result = [];to_avoid = avoid} | br::brl' -> (* alpha conversion to prevent name clashes *) - let _,(idl,patl,return) = alpha_br avoid br in + let {CAst.v=(idl,patl,return)} = alpha_br avoid br in let new_avoid = idl@avoid in (* for now we can no more use idl as an identifier *) (* building a list of precondition stating that we are not in this branch (will be used in the following recursive calls) @@ -948,7 +947,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) 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_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -983,7 +982,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 (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env @@ -995,7 +994,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = with Continue -> let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in - let ind,args' = Inductive.find_inductive env ty' in + let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in let mib,_ = Global.lookup_inductive (fst ind) in let nparam = mib.Declarations.mind_nparams in let params,arg' = @@ -1017,14 +1016,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; + let sigma = Evd.(from_env env) in let new_args = - match Constr.kind eq'_as_constr with + match EConstr.kind sigma eq'_as_constr with | App(_,[|_;_;ty;_|]) -> - let ty = Array.to_list (snd (destApp ty)) in + let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in let ty' = snd (Util.List.chop nparam ty) in List.fold_left2 (fun acc var_as_constr arg -> - let arg = EConstr.of_constr arg in if isRel var_as_constr then let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in @@ -1065,7 +1064,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in let new_env = let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in - Environ.push_rel (LocalAssum (n,t')) env + EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons @@ -1103,7 +1102,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); 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_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1119,7 +1118,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); 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_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1140,7 +1139,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1163,7 +1162,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = 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 (EConstr.of_constr t') in + let type_t' = Typing.unsafe_type_of env evd t' in + let t' = EConstr.Unsafe.to_constr t' in let type_t' = EConstr.Unsafe.to_constr type_t' in let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in let new_b,id_to_exclude = @@ -1189,7 +1189,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = depth t 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_env = EConstr.push_rel (LocalAssum (na,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1295,8 +1295,8 @@ let rec rebuild_return_type rt = CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt], + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt)], CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive @@ -1351,12 +1351,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1369,8 +1369,9 @@ 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 (LocalAssum (rel_name, - fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities + let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in + let rex = EConstr.Unsafe.to_constr rex in + Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = @@ -1418,12 +1419,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1450,18 +1451,18 @@ let do_build_inductive (fun (n,t,typ) -> match typ with | Some typ -> - Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t, + Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) | None -> Constrexpr.CLocalAssum - ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) + ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params in let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((Loc.tag id), + false,((CAst.make id), with_full_print (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t)) ) @@ -1469,7 +1470,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((Loc.tag @@ relnames.(i)), None), + (((CAst.make @@ relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index b4ca1073ca..40ea40b6b3 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -111,11 +111,11 @@ let change_vars = Miscops.map_cast_type (change_vars mapping) c) | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt - and change_vars_br mapping ((loc,(idl,patl,res)) as br) = + and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in if Id.Map.is_empty new_mapping then br - else (loc,(idl,patl,change_vars new_mapping res)) + else CAst.make ?loc (idl,patl,change_vars new_mapping res) in change_vars @@ -298,13 +298,13 @@ let rec alpha_rt excluded rt = in new_rt -and alpha_br excluded (loc,(ids,patl,res)) = +and alpha_br excluded {CAst.loc;v=(ids,patl,res)} = let new_patl,new_excluded,mapping = alpha_patl excluded patl in let new_ids = List.fold_right raw_get_pattern_id new_patl [] in let new_excluded = new_ids@excluded in let renamed_res = change_vars mapping res in let new_res = alpha_rt new_excluded renamed_res in - (loc,(new_ids,new_patl,new_res)) + CAst.make ?loc (new_ids,new_patl,new_res) (* [is_free_in id rt] checks if [id] is a free variable in [rt] @@ -348,7 +348,7 @@ let is_free_in id = | GCast (b,CastCoerce) -> is_free_in b | GProj (_,c) -> is_free_in c ) x - and is_free_in_br (_,(ids,_,rt)) = + and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt in is_free_in @@ -443,10 +443,10 @@ let replace_var_by_term x_id term = | GProj(p,c) -> GProj(p,replace_var_by_pattern c) ) x - and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = + and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl then br - else (loc,(idl,patl,replace_var_by_pattern res)) + else CAst.make ?loc (idl,patl,replace_var_by_pattern res) in replace_var_by_pattern @@ -547,8 +547,8 @@ let expand_as = List.map (expand_as_br map) brl) | GProj(p,c) -> GProj(p, expand_as map c) ) - and expand_as_br map (loc,(idl,cpl,rt)) = - (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) + and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} = + CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt) in expand_as Id.Map.empty @@ -562,7 +562,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* we first (pseudo) understand [rt] and get back the computed evar_map *) (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) - let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in + let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in let ctx, f = Evarutil.nf_evars_and_universes ctx in (* then we map [rt] to replace the implicit holes by their values *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 58154d3106..9c350483b3 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -93,7 +93,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,Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in @@ -141,8 +141,7 @@ let rec abstract_glob_constr c = function | Constrexpr.CLocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = - Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - c + Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls c (* Construct a fixpoint as a Glob_term @@ -155,14 +154,14 @@ let build_newrecursive let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (((_,recname),_),bl,arityc,_) -> + (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in - let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in + let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) + (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) @@ -216,7 +215,7 @@ let is_rec names = List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl | GProj(_,c) -> lookup names c - and lookup_br names (_,(idl,_,rt)) = + and lookup_br names {CAst.v=(idl,_,rt)} = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt in @@ -344,7 +343,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.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function (({CAst.v=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 @@ -357,7 +356,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in + let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in let ind_kn = fst (locate_with_msg (pr_reference f_R_mut++str ": Not an inductive type!") @@ -365,7 +364,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = Ident fname in + let f_ref = CAst.map (fun n -> Ident n) fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") locate_constant @@ -404,7 +403,7 @@ 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),pl),_,bl,ret_type,body),_] when not is_rec -> + | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false @@ -413,7 +412,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -430,7 +429,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -460,7 +459,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let rec_arg_num = let names = List.map - snd + CAst.(with_val (fun x -> x)) (Constrexpr_ops.names_of_local_assums args) in match wf_arg with @@ -473,17 +472,17 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,(Ident (Loc.tag fname)),None) , + (None,CAst.make @@ Ident fname,None) , (List.map (function - | _,Anonymous -> assert false - | _,Name e -> (Constrexpr_ops.mkIdentC e) + | {CAst.v=Anonymous} -> assert false + | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e) ) (Constrexpr_ops.names_of_local_assums args) ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -515,7 +514,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> begin match args with - | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x + | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -525,7 +524,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas (function | Constrexpr.CLocalAssum(l,k,t) -> List.exists - (function (_,Name id) -> Id.equal id wf_args | _ -> false) + (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false) l | _ -> false ) @@ -540,13 +539,13 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path + CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in - Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) + Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) in let wf_rel_from_mes = Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes]) @@ -557,7 +556,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let a = Names.Id.of_string "___a" in let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( - [Loc.tag @@ Name a;Loc.tag @@ Name b], + [CAst.make @@ Name a; CAst.make @@ Name b], Constrexpr.Default Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, @@ -591,11 +590,11 @@ and rebuild_nal aux bk bl' nal typ = match nal,typ with | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ | [], _ -> rebuild_bl aux bl' typ - | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> - if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') + | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> + if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v) then let assum = CLocalAssum([na],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -604,7 +603,7 @@ and rebuild_nal aux bk bl' nal typ = (CAst.make @@ CProdN(new_rest,typ')) else let assum = CLocalAssum([na'],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -638,7 +637,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),pl),_,args,types,body)),_) as fixpoint_expr = + let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -659,10 +658,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook; + then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) 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 (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -683,7 +682,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook; + then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; true | _ -> List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> @@ -696,7 +695,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 ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in @@ -725,23 +724,27 @@ let do_generate_principle pconstants on_error register_built interactive_proof let rec add_args id new_args = CAst.map (function | CRef (r,_) as b -> begin match r with - | Libnames.Ident(loc,fname) when Id.equal fname id -> + | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> CAppExpl((None,r,None),new_args) | _ -> b end | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> - CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLambdaN(nal,b1) -> - CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) | CAppExpl((pf,r,us),exprl) -> begin match r with - | Libnames.Ident(loc,fname) when Id.equal fname id -> + | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) end @@ -753,7 +756,7 @@ let rec add_args id new_args = CAst.map (function List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal + List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal ) | CLetTuple(nal,(na,b_option),b1,b2) -> CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), @@ -793,7 +796,7 @@ let rec chop_n_arrow n t = then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) match t.CAst.v with - | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : + | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on the remaining number of arrow to chop and [t'] we discard it and @@ -805,7 +808,7 @@ let rec chop_n_arrow n t = let new_n = let rec aux (n:int) = function [] -> n - | (nal,k,t'')::nal_ta' -> + | CLocalAssum(nal,k,t'')::nal_ta' -> let nal_l = List.length nal in if n >= nal_l then @@ -813,9 +816,10 @@ let rec chop_n_arrow n t = else let new_t' = CAst.make @@ Constrexpr.CProdN( - ((snd (List.chop n nal)),k,t'')::nal_ta',t') + CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') + | _ -> anomaly (Pp.str "Not enough products.") in aux n nal_ta' in @@ -828,16 +832,13 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b.CAst.v with - | Constrexpr.CLambdaN ((nal_ta), b') -> + | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') -> begin - let n = - (List.fold_left (fun n (nal,_,_) -> - n+List.length nal) 0 nal_ta ) - in - let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in - (List.map (fun (nal,k,ta) -> - (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + let n = List.length nal in + let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in + d :: nal_tas, b'',t'' end + | Constrexpr.CLambdaN ([], b) -> [],b,t | _ -> [],b,t @@ -873,7 +874,7 @@ let make_graph (f_ref:global_reference) = let l = List.map (fun (id,(n,recexp),bl,t,b) -> - let loc, rec_id = Option.get n in + let { CAst.loc; v=rec_id } = Option.get n in let new_args = List.flatten (List.map @@ -881,29 +882,29 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> CAst.make ?loc @@ - CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ + CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false ) nal_tas ) in - let b' = add_args (snd id) new_args b in - ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + let b' = add_args id.CAst.v new_args b in + ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixexprl in l | _ -> let id = Label.to_id (Constant.label c) in - [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp,dp,_ = Constant.repr3 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 (Constant.make3 mp dp (Label.of_id id))) + (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) expr_list) let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 93e03852ec..dcc1c2ea6a 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -14,7 +14,7 @@ val functional_induction : bool -> EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> - Tacexpr.or_and_intro_pattern option -> + Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index d6fd2f2a0f..a0b9217c75 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -32,7 +32,7 @@ let id_of_name = function | _ -> raise Not_found let locate ref = - let (loc,qid) = qualid_of_reference ref in + let {CAst.v=qid} = qualid_of_reference ref in Nametab.locate qid let locate_ind ref = @@ -100,13 +100,8 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l - - - let const_of_id id = - let _,princ_ref = - qualid_of_reference (Libnames.Ident (Loc.tag id)) - in + let princ_ref = qualid_of_ident id in try Constrintern.locate_reference princ_ref with Not_found -> CErrors.user_err ~hdr:"IndFun.const_of_id" diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 4acf82d000..2743a8a2f9 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Ltac_plugin @@ -238,7 +240,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.map (fun decl -> List.map - (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id)) + (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -254,7 +256,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i (* We get the identifiers of this branch *) let pre_args = List.fold_right - (fun (_,pat) acc -> + (fun {CAst.v=pat} acc -> match pat with | IntroNaming (IntroIdentifier id) -> id::acc | _ -> anomaly (Pp.str "Not an identifier.") diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index e07138596c..ad306ab257 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) val invfun : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8fe05b4978..fb9ae64bf4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -204,12 +206,13 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) = (RegularStyle,None, [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in + let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = @@ -896,8 +899,8 @@ let rec make_rewrite_list expr_info max = function Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); - Loc.tag @@ (NamedHyp k, f_S max)]) false) g) ) + ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); + CAst.make @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) @@ -923,8 +926,8 @@ let make_rewrite expr_info l hp max = (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); - Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g) + ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); + CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ @@ -1322,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = Libnames.Ident (Loc.tag na) in + let na_ref = CAst.make @@ Libnames.Ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1400,7 +1403,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp (fun c -> Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [intros; - Simple.apply (EConstr.of_constr (fst (interp_constr (Global.env()) Evd.empty c))) (*FIXME*); + Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*); Tacticals.New.tclCOMPLETE Auto.default_auto ]) ) @@ -1576,7 +1579,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); @@ -1599,7 +1602,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation); + functional_ref eq_ref rec_arg_num + (EConstr.of_constr rec_arg_type) + (nb_prod evd (EConstr.of_constr res)) relation; Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ @@ -1614,7 +1619,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num tcc_lemma_constr is_mes functional_ref (EConstr.of_constr rec_arg_type) - (EConstr.of_constr relation) rec_arg_num + relation rec_arg_num term_id using_lemmas (List.length res_vars) |