diff options
Diffstat (limited to 'plugins')
37 files changed, 400 insertions, 315 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 575d964158..23cdae7883 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -17,6 +17,7 @@ open Pp open Names open Sorts open Constr +open Context open Vars open Goptions open Tacmach @@ -421,11 +422,11 @@ let new_representative typ = let _A_ = Name (Id.of_string "A") let _B_ = Name (Id.of_string "A") -let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2) +let _body_ = mkProd(make_annot Anonymous Sorts.Relevant,mkRel 2,mkRel 2) let cc_product s1 s2 = - mkLambda(_A_,mkSort(s1), - mkLambda(_B_,mkSort(s2),_body_)) + mkLambda(make_annot _A_ Sorts.Relevant,mkSort(s1), + mkLambda(make_annot _B_ Sorts.Relevant,mkSort(s2),_body_)) let rec constr_of_term = function Symb s-> s @@ -452,11 +453,11 @@ let rec canonize_name sigma c = let canon_mind = MutInd.make1 (MutInd.canonical kn) in mkConstructU (((canon_mind,i),j),u) | Prod (na,t,ct) -> - mkProd (na,func t, func ct) + mkProd (na,func t, func ct) | Lambda (na,t,ct) -> - mkLambda (na, func t,func ct) + mkLambda (na, func t,func ct) | LetIn (na,b,t,ct) -> - mkLetIn (na, func b,func t,func ct) + mkLetIn (na, func b,func t,func ct) | App (ct,l) -> mkApp (func ct,Array.Smart.map func l) | Proj(p,c) -> @@ -806,7 +807,8 @@ let __eps__ = Id.of_string "_eps_" let new_state_var typ state = let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in let id = Namegen.next_ident_away __eps__ ids in - state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env; + let r = Sorts.Relevant in (* TODO relevance *) + state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env; id let complete_one_class state i= @@ -814,9 +816,9 @@ let complete_one_class state i= Partial pac -> let rec app t typ n = if n<=0 then t else - let _,etyp,rest= destProd typ in + let _,etyp,rest= destProd typ in let id = new_state_var (EConstr.of_constr etyp) state in - app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in + app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in let _c = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in let _c = EConstr.Unsafe.to_constr _c in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 055d36747d..5778acce0a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -15,6 +15,7 @@ open Names open Inductiveops open Declarations open Constr +open Context open EConstr open Vars open Tactics @@ -151,19 +152,19 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match EConstr.kind sigma (whd_delta env sigma term) with - Prod (id,atom,ff) -> + Prod (id,atom,ff) -> if is_global sigma (Lazy.force _False) ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts let litteral_of_constr env sigma term= match EConstr.kind sigma (whd_delta env sigma term) with - | Prod (id,atom,ff) -> + | Prod (id,atom,ff) -> if is_global sigma (Lazy.force _False) ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) @@ -171,7 +172,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff + quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -233,7 +234,7 @@ let build_projection intype (cstr:pconstructor) special default gls= let sigma = project gls in let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in - sigma, mkLambda(Name id,intype,body) + sigma, mkLambda(make_annot (Name id) Sorts.Relevant,intype,body) (* generate an adhoc tactic following the proof tree *) @@ -318,7 +319,7 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of tx1) (fun typx -> refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in - let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in + let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in let prf = @@ -377,7 +378,7 @@ let convert_to_goal_tac c t1 t2 p = let neweq= app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in - let identity=mkLambda (Name x,sort,mkRel 1) in + let identity=mkLambda (make_annot (Name x) Sorts.Relevant,sort,mkRel 1) in let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; endt refine_exact_check] diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index d06a241969..afdbfa1999 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -9,6 +9,7 @@ (************************************************************************) open Constr +open Context open Context.Named.Declaration let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) @@ -39,7 +40,7 @@ let start_deriving f suchthat lemma = TCons ( env , sigma , f_type , (fun sigma ef -> let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in - let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in + let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index b59e3b608c..0fa9be21c9 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -150,7 +150,7 @@ let check_fix env sg cb i = | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) = - Array.equal Name.equal na1 na2 && + Array.equal (Context.eq_annot Name.equal) na1 na2 && Array.equal (EConstr.eq_constr sg) ca1 ca2 && Array.equal (EConstr.eq_constr sg) ta1 ta2 diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ef6c07bff2..c9cfd74362 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -13,6 +13,7 @@ open Util open Names open Term open Constr +open Context open Declarations open Declareops open Environ @@ -73,13 +74,18 @@ type flag = info * scheme (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) +let info_of_family = function + | InSProp | InProp -> Logic + | InSet | InType -> Info + +let info_of_sort s = info_of_family (Sorts.family s) + let rec flag_of_type env sg t : flag = let t = whd_all env sg t in match EConstr.kind sg t with | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c - | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme) - | Sort _ -> (Info,TypeScheme) - | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default) + | Sort s -> (info_of_sort (EConstr.ESorts.kind sg s),TypeScheme) + | _ -> (info_of_family (sort_of env sg t),Default) (*s Two particular cases of [flag_of_type]. *) @@ -179,7 +185,7 @@ let rec type_sign_vl env sg c = | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) sg d in if not (is_info_scheme env sg t) then Kill Kprop::s, vl - else Keep::s, (make_typvar n vl) :: vl + else Keep::s, (make_typvar n.binder_name vl) :: vl | _ -> [],[] let rec nb_default_params env sg c = @@ -259,14 +265,14 @@ let rec extract_type env sg db j c args = (* We just accumulate the arguments. *) extract_type env sg db j d (Array.to_list args' @ args) | Lambda (_,_,d) -> - (match args with + (match args with | [] -> assert false (* A lambda cannot be a type. *) | a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args) | Prod (n,t,d) -> - assert (List.is_empty args); - let env' = push_rel_assum (n,t) env in + assert (List.is_empty args); + let env' = push_rel_assum (n,t) env in (match flag_of_type env sg t with - | (Info, Default) -> + | (Info, Default) -> (* Standard case: two [extract_type] ... *) let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with @@ -291,7 +297,7 @@ let rec extract_type env sg db j c args = (match EConstr.lookup_rel n env with | LocalDef (_,t,_) -> extract_type env sg db j (EConstr.Vars.lift n t) args - | _ -> + | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown else let n' = List.nth db (n-1) in @@ -492,8 +498,8 @@ and extract_really_ind env kn mib = (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match Constr.kind t with - | Prod(n,_,t) -> n::(names_prod t) - | LetIn(_,_,_,t) -> names_prod t + | Prod(n,_,t) -> n::(names_prod t) + | LetIn(_,_,_,t) -> names_prod t | Cast(t,_,_) -> names_prod t | _ -> [] in @@ -506,9 +512,9 @@ and extract_really_ind env kn mib = | [],[] -> [] | _::l, typ::typs when isTdummy (expand env typ) -> select_fields l typs - | Anonymous::l, typ::typs -> + | {binder_name=Anonymous}::l, typ::typs -> None :: (select_fields l typs) - | Name id::l, typ::typs -> + | {binder_name=Name id}::l, typ::typs -> let knp = Constant.make2 mp (Label.of_id id) in (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((==) Keep) (type2signature env typ) @@ -551,8 +557,8 @@ and extract_really_ind env kn mib = and extract_type_cons env sg db dbmap c i = match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let env' = push_rel_assum (n,t) env in - let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in + let env' = push_rel_assum (n,t) env in + let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in let l = extract_type_cons env' sg db' dbmap d (i+1) in (extract_type env sg db 0 t []) :: l | _ -> [] @@ -615,17 +621,18 @@ let rec extract_term env sg mle mlt c args = | App (f,a) -> extract_term env sg mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> - let id = id_of_name n in + let id = map_annot id_of_name n in + let idna = map_annot Name.mk_name id in (match args with | a :: l -> (* We make as many [LetIn] as possible. *) let l' = List.map (EConstr.Vars.lift 1) l in - let d' = EConstr.mkLetIn (Name id,a,t,applistc d l') in + let d' = EConstr.mkLetIn (idna,a,t,applistc d l') in extract_term env sg mle mlt d' [] - | [] -> - let env' = push_rel_assum (Name id, t) env in + | [] -> + let env' = push_rel_assum (idna, t) env in let id, a = - try check_default env sg t; Id id, new_meta() + try check_default env sg t; Id id.binder_name, new_meta() with NotDefault d -> Dummy, Tdummy d in let b = new_meta () in @@ -634,9 +641,9 @@ let rec extract_term env sg mle mlt c args = let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> - let id = id_of_name n in - let env' = EConstr.push_rel (LocalDef (Name id, c1, t1)) env in - (* We directly push the args inside the [LetIn]. + let id = map_annot id_of_name n in + let env' = EConstr.push_rel (LocalDef (map_annot Name.mk_name id, c1, t1)) env in + (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) let args' = List.map (EConstr.Vars.lift 1) args in (try @@ -649,7 +656,7 @@ let rec extract_term env sg mle mlt c args = then Mlenv.push_gen mle a else Mlenv.push_type mle a in - MLletin (Id id, c1', extract_term env' sg mle' mlt c2 args') + MLletin (Id id.binder_name, c1', extract_term env' sg mle' mlt c2 args') with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' sg mle' mlt c2 args')) @@ -913,7 +920,7 @@ and extract_fix env sg mle i (fi,ti,ci as recd) mlt = metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in let ei = Array.map2 (extract_maybe_term env sg mle) metas ci in - MLfix (i, Array.map id_of_name fi, ei) + MLfix (i, Array.map (fun x -> id_of_name x.binder_name) fi, ei) (*S ML declarations. *) @@ -989,7 +996,7 @@ let extract_std_constant env sg kn body typ = (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in (* The lambdas names. *) - let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in + let ids = List.map (fun (n,_) -> Id (id_of_name n.binder_name)) rels in (* The according Coq environment. *) let env = push_rels_assum rels env in (* The real extraction: *) @@ -1055,12 +1062,15 @@ let fake_match_projection env p = ci_npar = mib.mind_nparams; ci_cstr_ndecls = mip.mind_consnrealdecls; ci_cstr_nargs = mip.mind_consnrealargs; + ci_relevance = Declareops.relevance_of_projection_repr mib p; ci_pp_info; } in let x = match mib.mind_record with | NotRecord | FakeRecord -> assert false - | PrimRecord info -> Name (pi1 info.(snd ind)) + | PrimRecord info -> + let x, _, _, _ = info.(snd ind) in + make_annot (Name x) mip.mind_relevance in let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in let rec fold arg j subst = function @@ -1068,7 +1078,7 @@ let fake_match_projection env p = | LocalAssum (na,ty) :: rem -> let ty = Vars.substl subst (liftn 1 j ty) in if arg != proj_arg then - let lab = match na with Name id -> Label.of_id id | Anonymous -> assert false in + let lab = match na.binder_name with Name id -> Label.of_id id | Anonymous -> assert false in let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem else diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2058837b8e..399a77c596 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -449,11 +449,11 @@ let argnames_of_global r = let typ, _ = Typeops.type_of_global_in_context env r in let rels,_ = decompose_prod (Reduction.whd_all env typ) in - List.rev_map fst rels + List.rev_map (fun x -> Context.binder_name (fst x)) rels let msg_of_implicit = function | Kimplicit (r,i) -> - let name = match List.nth (argnames_of_global r) (i-1) with + let name = match (List.nth (argnames_of_global r) (i-1)) with | Anonymous -> "" | Name id -> "(" ^ Id.to_string id ^ ") " in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 286021d68e..1c9ab2e3bd 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance env evmap id idc m t = (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd evmap (whd_all env evmap typ) in - match nam with + match nam.Context.binder_name with Name id -> id | Anonymous -> dummy_bvid in let revt=substl (List.init m (fun i->mkRel (m-i))) t in @@ -115,7 +115,7 @@ let mk_open_instance env evmap id idc m t = if Int.equal n 0 then evmap, decls else let nid=(fresh_id_in_env avoid var_id env) in let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let decl = LocalAssum (Name nid, c) in + let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m Id.Set.empty env evmap [] in (evmap, decls, revt) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 832a98b7f8..7f06ab6777 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -163,9 +163,9 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq = let ll_arrow_tac a b c backtrack id continue seq= let open EConstr in let open Vars in - let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d idc = mkLambda (Anonymous,b, - mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + let cc=mkProd(Context.make_annot Anonymous Sorts.Relevant,a,(lift 1 b)) in + let d idc = mkLambda (Context.make_annot Anonymous Sorts.Relevant,b, + mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in tclORELSE (tclTHENS (cut c) [tclTHENLIST diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index d63fe9d799..0c958ddee3 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -65,13 +65,13 @@ let unif evd t1 t2= bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige - | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> + | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; let l=Array.length va in - if not (Int.equal l (Array.length vb)) then + if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else for i=0 to l-1 do diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 6fd2f7c2bc..34283c49c3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -2,6 +2,7 @@ open Printer open CErrors open Util open Constr +open Context open EConstr open Vars open Namegen @@ -302,7 +303,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = in let old_context_length = List.length context + 1 in let witness_fun = - mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t, + mkLetIn(make_annot Anonymous Sorts.Relevant,make_refl_eq constructor t1_typ (fst t1),t, mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i))) ) in @@ -312,7 +313,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) + (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_annot decl, + witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -428,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = else if isProd sigma type_of_hyp then begin - let (x,t_x,t') = destProd sigma type_of_hyp in + let (x,t_x,t') = destProd sigma type_of_hyp in let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in if is_property sigma ptes_infos t_x actual_real_type_of_hyp then begin @@ -541,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (scan_type new_context new_t') with NoChange -> (* Last thing todo : push the rel in the context and continue *) - scan_type (LocalAssum (x,t_x) :: context) t' + scan_type (LocalAssum (x,t_x) :: context) t' end end else @@ -610,7 +612,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = anomaly (Pp.str "cannot compute new term value.") in let fun_body = - mkLambda(Anonymous, + mkLambda(make_annot Anonymous Sorts.Relevant, pf_unsafe_type_of g' term, Termops.replace_term (project g') term (mkRel 1) dyn_infos.info ) @@ -736,7 +738,7 @@ let build_proof g in build_proof do_finalize_t {dyn_infos with info = t} g - | Lambda(n,t,b) -> + | Lambda(n,t,b) -> begin match EConstr.kind sigma (pf_concl g) with | Prod _ -> @@ -1149,7 +1151,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let fix_offset = List.length princ_params in let ptes_to_fix,infos = match EConstr.kind (project g) fbody_with_full_params with - | Fix((idxs,i),(names,typess,bodies)) -> + | Fix((idxs,i),(names,typess,bodies)) -> let bodies_with_all_params = Array.map (fun body -> @@ -1164,7 +1166,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (fun i types -> let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; - name = Nameops.Name.get_id (fresh_id names.(i)); + name = Nameops.Name.get_id (fresh_id names.(i).binder_name); types = types; offset = fix_offset; nb_realargs = @@ -1195,9 +1197,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam applist(body,List.rev_map var_of_decl full_params)) in match EConstr.kind (project g) body_with_full_params with - | Fix((_,num),(_,_,bs)) -> + | Fix((_,num),(_,_,bs)) -> Reductionops.nf_betaiota (pf_env g) (project g) - ( + ( (applist (substl (List.rev @@ -1514,7 +1516,7 @@ let is_valid_hypothesis sigma predicates_name = let rec is_valid_hypothesis typ = is_pte typ || match EConstr.kind sigma typ with - | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' + | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' | _ -> false in is_valid_hypothesis @@ -1565,7 +1567,7 @@ let prove_principle_for_gen in let rec_arg_id = match List.rev post_rec_arg with - | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id + | (LocalAssum ({binder_name=Name id},_) | LocalDef ({binder_name=Name id},_,_)) :: _ -> id | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index ca09cad1f3..1217ba0eba 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -14,6 +14,7 @@ open Term open Sorts open Util open Constr +open Context open Vars open Namegen open Names @@ -72,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = then List.tl args else args in - Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl), + Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl), Term.compose_prod real_args (mkSort new_sort)) in let new_predicates = @@ -137,14 +138,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Rel n -> begin try match Environ.lookup_rel n env with - | LocalAssum (_,t) | LocalDef (_,_,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 - | Prod(x,t,b) -> - compute_new_princ_type_for_binder remove mkProd env x t b - | Lambda(x,t,b) -> - compute_new_princ_type_for_binder remove mkLambda env x t b + | Prod(x,t,b) -> + compute_new_princ_type_for_binder remove mkProd env x t b + | Lambda(x,t,b) -> + compute_new_princ_type_for_binder remove mkLambda env x t b | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved | App(f,args) when is_dom f -> let var_to_be_removed = destRel (Array.last args) in @@ -164,8 +165,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in applistc new_f new_args, list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove - | LetIn(x,v,t,b) -> - compute_new_princ_type_for_letin remove env x v t b + | LetIn(x,v,t,b) -> + compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in (* let _ = match Constr.kind pre_princ with *) @@ -181,14 +182,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = begin 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 (LocalAssum (x,t)) env in + let new_x = map_annot (get_name (Termops.ids_of_context env)) x 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 (Constr.equal (mkRel 1)) binders_to_remove_from_b then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( - bind_fun(new_x,new_t,new_b), + bind_fun(new_x,new_t,new_b), list_union_eq Constr.equal binders_to_remove_from_t @@ -210,14 +211,14 @@ 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_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 (LocalDef (x,v,t)) env in + let new_x = map_annot (get_name (Termops.ids_of_context env)) x 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 (Constr.equal (mkRel 1)) binders_to_remove_from_b then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( - mkLetIn(new_x,new_v,new_t,new_b), + mkLetIn(new_x,new_v,new_t,new_b), list_union_eq Constr.equal (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) @@ -250,8 +251,11 @@ 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 (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)) + pre_res (List.map (function + | Context.Named.Declaration.LocalAssum (id,b) -> + LocalAssum (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, b) + | Context.Named.Declaration.LocalDef (id,t,b) -> + LocalDef (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, t, b)) new_predicates) ) (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params) @@ -264,7 +268,7 @@ let change_property_sort evd toSort princ princName = let princ_info = compute_elim_sig evd princ in let change_sort_in_predicate decl = LocalAssum - (get_name decl, + (get_annot decl, let args,ty = decompose_prod (EConstr.Unsafe.to_constr (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); @@ -414,7 +418,7 @@ let get_funs_constant mp = | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> - match na with + match na.binder_name with | Name id -> let const = Constant.make2 mp (Label.of_id id) in const,i @@ -451,7 +455,8 @@ let get_funs_constant mp = let first_params = List.hd l_params in List.iter (fun params -> - if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params) + if not (List.equal (fun (n1, c1) (n2, c2) -> + eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params) then user_err Pp.(str "Not a mutal recursive block") ) l_params @@ -461,7 +466,7 @@ let get_funs_constant mp = try let extract_info is_first body = match Constr.kind body with - | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) + | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) | _ -> if is_first && Int.equal (List.length l_bodies) 1 then raise Not_Rec @@ -469,9 +474,9 @@ let get_funs_constant mp = in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) - let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = - Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 && - Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 + let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = + Array.equal Int.equal ia1 ia2 && Array.equal (eq_annot Name.equal) na1 na2 && + Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) then user_err Pp.(str "Not a mutal recursive block") diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index ba0a3bbb5c..8611dcaf83 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -2,6 +2,7 @@ open Printer open Pp open Names open Constr +open Context open Vars open Glob_term open Glob_ops @@ -343,12 +344,13 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + let na = make_annot id Sorts.Relevant in (* TODO relevance *) (match raw_value with | None -> - EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env + EConstr.push_named (NamedDecl.LocalAssum (na,typ)) env | Some value -> - EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env) + EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env) let add_pat_variables pat typ env : Environ.env = @@ -356,7 +358,7 @@ let add_pat_variables pat typ env : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match DAst.get pat with - | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env + | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (make_annot na Sorts.Relevant,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) @@ -375,16 +377,18 @@ let add_pat_variables pat typ env : Environ.env = let open Context.Rel.Declaration in let sigma, _ = Pfedit.get_current_context () in match decl with - | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false - | LocalAssum (Name id, t) -> + | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false + | LocalAssum ({binder_name=Name id} as na, t) -> + let na = {na with binder_name=id} in let new_t = substl ctxt t in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) - | LocalDef (Name id, v, t) -> + (Environ.push_named (LocalAssum (na,new_t)) env,mkVar id::ctxt) + | LocalDef ({binder_name=Name id} as na, v, t) -> + let na = {na with binder_name=id} in let new_t = substl ctxt t in let new_v = substl ctxt v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ @@ -394,7 +398,7 @@ let add_pat_variables pat typ env : Environ.env = str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + (Environ.push_named (LocalDef (na,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) @@ -626,11 +630,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = 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) v_as_constr in + let v_r = Sorts.Relevant in (* TODO relevance *) let new_env = match n with Anonymous -> env - | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env - in + | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,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 | GCases(_,_,el,brl) -> @@ -939,9 +944,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = 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 = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -974,9 +980,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_args = List.map (replace_var_by_term id rt) args in let subst_b = if is_in_b then b else replace_var_by_term id rt b - in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + in + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1057,8 +1064,9 @@ 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 - EConstr.push_rel (LocalAssum (n,t')) env - in + let r = Sorts.Relevant in (* TODO relevance *) + EConstr.push_rel (LocalAssum (make_annot n r,t')) env + in let new_b,id_to_exclude = rebuild_cons new_env @@ -1095,8 +1103,9 @@ 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 = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -1111,8 +1120,9 @@ 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 = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -1132,8 +1142,9 @@ 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 = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname (args@[mkGVar id])new_crossed_types @@ -1158,7 +1169,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = 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_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1182,8 +1193,9 @@ 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 = EConstr.push_rel (LocalAssum (na,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot na r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args (t::crossed_types) @@ -1320,7 +1332,7 @@ let do_build_inductive let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in let t = EConstr.Unsafe.to_constr t in evd, - Environ.push_named (LocalAssum (id,t)) + Environ.push_named (LocalAssum (make_annot id Sorts.Relevant,t)) env ) funnames @@ -1364,7 +1376,8 @@ let do_build_inductive Util.Array.fold_left2 (fun env rel_name rel_ar -> 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 + let r = Sorts.Relevant in (* TODO relevance *) + Environ.push_named (LocalAssum (make_annot rel_name r,rex)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 42dc66dcf4..b69ca7080c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -3,6 +3,7 @@ open Sorts open Util open Names open Constr +open Context open EConstr open Pp open Indfun_common @@ -49,7 +50,8 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction information on "++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in - match Tacticals.elimination_sort_of_goal g with + match Tacticals.elimination_sort_of_goal g with + | InSProp -> finfo.sprop_lemma | InProp -> finfo.prop_lemma | InSet -> finfo.rec_lemma | InType -> finfo.rect_lemma @@ -169,7 +171,8 @@ let build_newrecursive let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in - (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) + let r = Sorts.Relevant in (* TODO relevance *) + (EConstr.push_named (LocalAssum (make_annot recname r,arity)) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) @@ -621,8 +624,8 @@ let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in - let constr_expr_typel = + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in + let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) 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 -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index cba3cc3d42..88546e9ae8 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -199,6 +199,7 @@ type function_info = rect_lemma : Constant.t option; rec_lemma : Constant.t option; prop_lemma : Constant.t option; + sprop_lemma : Constant.t option; is_general : bool; (* Has this function been defined using general recursive definition *) } @@ -249,6 +250,7 @@ let subst_Function (subst,finfos) = let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in + let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -256,7 +258,8 @@ let subst_Function (subst,finfos) = completeness_lemma' == finfos.completeness_lemma && rect_lemma' == finfos.rect_lemma && rec_lemma' == finfos.rec_lemma && - prop_lemma' == finfos.prop_lemma + prop_lemma' == finfos.prop_lemma && + sprop_lemma' == finfos.sprop_lemma then finfos else { function_constant = function_constant'; @@ -267,6 +270,7 @@ let subst_Function (subst,finfos) = rect_lemma = rect_lemma' ; rec_lemma = rec_lemma'; prop_lemma = prop_lemma'; + sprop_lemma = sprop_lemma'; is_general = finfos.is_general } @@ -333,6 +337,7 @@ let add_Function is_general f = and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect") and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec") and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") + and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") @@ -345,6 +350,7 @@ let add_Function is_general f = rect_lemma = rect_lemma; rec_lemma = rec_lemma; prop_lemma = prop_lemma; + sprop_lemma = sprop_lemma; graph_ind = graph_ind; is_general = is_general diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 1e0b95df34..4ec3131518 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -70,6 +70,7 @@ type function_info = rect_lemma : Constant.t option; rec_lemma : Constant.t option; prop_lemma : Constant.t option; + sprop_lemma : Constant.t option; is_general : bool; } @@ -109,9 +110,9 @@ val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_referenc val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> - (Names.Name.t * EConstr.t) list * EConstr.t -val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t -val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t + (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t +val compose_lam : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t +val compose_prod : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t type tcc_lemma_value = | Undefined diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 95e2e9f6e5..37dbfec4c9 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -15,6 +15,7 @@ open Util open Names open Term open Constr +open Context open EConstr open Vars open Pp @@ -142,12 +143,13 @@ 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 = - LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt + LocalAssum (make_annot (Name res_id) Sorts.Relevant, lift 1 res_type) :: + LocalDef (make_annot (Name fv_id) Sorts.Relevant, 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 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 + then LocalAssum (make_annot Anonymous Sorts.Relevant,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph + else LocalAssum (make_annot Anonymous Sorts.Relevant,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph (* @@ -270,10 +272,10 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let type_of_hid = pf_unsafe_type_of g (mkVar hid) in let sigma = project g in match EConstr.kind sigma type_of_hid with - | Prod(_,_,t') -> + | Prod(_,_,t') -> begin match EConstr.kind sigma t' with - | Prod(_,t'',t''') -> + | Prod(_,t'',t''') -> begin match EConstr.kind sigma t'',EConstr.kind sigma t''' with | App(eq,args), App(graph',_) @@ -358,17 +360,16 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i (* end of branche proof *) let lemmas = Array.map - (fun ((_,(ctxt,concl))) -> - match ctxt with - | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") - | hres::res::decl::ctxt -> - let res = EConstr.it_mkLambda_or_LetIn - (EConstr.it_mkProd_or_LetIn concl [hres;res]) - (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) - in - res - ) - lemmas_types_infos + (fun ((_,(ctxt,concl))) -> + match ctxt with + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") + | hres::res::decl::ctxt -> + let res = EConstr.it_mkLambda_or_LetIn + (EConstr.it_mkProd_or_LetIn concl [hres;res]) + (LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl) :: ctxt) + in + res) + lemmas_types_infos in let param_names = fst (List.chop princ_infos.nparams args_names) in let params = List.map mkVar param_names in @@ -429,7 +430,7 @@ let generalize_dependent_of x hyp g = let open Context.Named.Declaration in tclMAP (function - | LocalAssum (id,t) when not (Id.equal id hyp) && + | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) && (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) | _ -> tclIDTAC ) @@ -456,7 +457,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = let eq_ind = make_eq () in let sigma = project g in match EConstr.kind sigma (pf_concl g) with - | Prod(_,t,t') -> + | Prod(_,t,t') -> begin match EConstr.kind sigma t with | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind) -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8746c37309..988cae8fbf 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -12,6 +12,7 @@ module CVars = Vars open Constr +open Context open EConstr open Vars open Namegen @@ -182,7 +183,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = ) in let context = List.map - (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al)) + (fun (x, c) -> LocalAssum (make_annot (Name x) Sorts.Relevant, c)) (List.combine rev_x_id_l (List.rev al)) in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = @@ -388,9 +389,9 @@ let add_vars sigma forbidden e = let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = fun g -> let rev_context,b = decompose_lam_n (project g) nb_lam e in - let ids = List.fold_left (fun acc (na,_) -> + let ids = List.fold_left (fun acc (na,_) -> let pre_id = - match na with + match na.binder_name with | Name x -> x | Anonymous -> ano_id in @@ -433,10 +434,10 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") | Proj _ -> user_err Pp.(str "Function cannot treat projections") - | LetIn(na,b,t,e) -> + | LetIn(na,b,t,e) -> begin let new_continuation_tac = - jinfo.letiN (na,b,t,e) expr_info continuation_tac + jinfo.letiN (na.binder_name,b,t,e) expr_info continuation_tac in travel jinfo new_continuation_tac {expr_info with info = b; is_final=false} g @@ -450,7 +451,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = with e when CErrors.noncritical e -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end - | Lambda(n,t,b) -> + | Lambda(n,t,b) -> begin try check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; @@ -853,8 +854,8 @@ let rec prove_le g = EConstr.is_global sigma (le ()) c | _ -> false in - let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) - in + let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in + let h = h.binder_name in let y = let _,args = decompose_app sigma t in List.hd (List.tl args) @@ -877,10 +878,10 @@ let rec make_rewrite_list expr_info max = function let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in let k,def = - let k_na,_,t = destProd sigma t_eq in - let _,_,t = destProd sigma t in - let def_na,_,_ = destProd sigma t in - Nameops.Name.get_id k_na,Nameops.Name.get_id def_na + let k_na,_,t = destProd sigma t_eq in + let _,_,t = destProd sigma t in + let def_na,_,_ = destProd sigma t in + Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true @@ -903,10 +904,10 @@ let make_rewrite expr_info l hp max = let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in let k,def = - let k_na,_,t = destProd sigma t_eq in - let _,_,t = destProd sigma t in - let def_na,_,_ = destProd sigma t in - Nameops.Name.get_id k_na,Nameops.Name.get_id def_na + let k_na,_,t = destProd sigma t_eq in + let _,_,t = destProd sigma t in + let def_na,_,_ = destProd sigma t in + Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name in observe_tac (str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences @@ -1054,20 +1055,19 @@ let compute_terminate_type nb_args func = let right = mkRel 5 in let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in - let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in + let result = (mkProd (make_annot (Name def_id) Sorts.Relevant, lift 4 a_arrow_b, equality)) in let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in let nb_iter = mkApp(delayed_force ex, [|delayed_force nat; (mkLambda - (Name - p_id, + (make_annot (Name p_id) Sorts.Relevant, delayed_force nat, - (mkProd (Name k_id, delayed_force nat, - mkArrow cond result))))|])in + (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat, + mkArrow cond Sorts.Relevant result))))|])in let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref), [|b; - (mkLambda (Name v_id, b, nb_iter))|]) in + (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in compose_prod rev_args value @@ -1165,15 +1165,15 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let func_body = EConstr.of_constr func_body in let (f_name, _, body1) = destLambda sigma func_body in let f_id = - match f_name with + match f_name.binder_name with | Name f_id -> next_ident_away_in_goal f_id ids | Anonymous -> anomaly (Pp.str "Anonymous function.") in let n_names_types,_ = decompose_lam_n sigma nb_args body1 in let n_ids,ids = List.fold_left - (fun (n_ids,ids) (n_name,_) -> - match n_name with + (fun (n_ids,ids) (n_name,_) -> + match n_name.binder_name with | Name id -> let n_id = next_ident_away_in_goal id ids in n_id::n_ids,n_id::ids @@ -1270,12 +1270,12 @@ let is_rec_res id = let clear_goals sigma = let rec clear_goal t = match EConstr.kind sigma t with - | Prod(Name id as na,t',b) -> + | Prod({binder_name=Name id} as na,t',b) -> let b' = clear_goal b in if noccurn sigma 1 b' && (is_rec_res id) then Vars.lift (-1) b' else if b' == b then t - else mkProd(na,t',b') + else mkProd(na,t',b') | _ -> EConstr.map sigma clear_goal t in List.map clear_goal @@ -1519,7 +1519,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = Evd.from_env env in let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in - let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let function_r = Sorts.Relevant in (* TODO relevance *) + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot function_name function_r,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in @@ -1537,7 +1538,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) match Constr.kind eq' with | App(e,[|_;_;eq_fix|]) -> - mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) + mkLambda (make_annot (Name function_name) Sorts.Relevant,function_type,subst_var function_name (compose_lam res_vars eq_fix)) | _ -> failwith "Recursive Definition (res not eq)" in let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index b0277e9cc2..050fdcb608 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -11,6 +11,7 @@ open Util open Names open Constr +open Context open CErrors open Evar_refiner open Tacmach @@ -62,7 +63,7 @@ let instantiate_tac n c ido = evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl)) | InHypValueOnly -> (match decl with - | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) + | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) | _ -> user_err Pp.(str "Not a defined hypothesis.")) in if List.length evl < n then user_err Pp.(str "Not enough uninstantiated existential variables."); @@ -108,5 +109,6 @@ let hget_evar n = if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in - Tactics.change_concl (mkLetIn (Name.Anonymous,mkEvar ev,ev_type,concl)) + let r = Retyping.relevance_of_type (Proofview.Goal.env gl) sigma ev_type in + Tactics.change_concl (mkLetIn (make_annot Name.Anonymous r,mkEvar ev,ev_type,concl)) end diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index ffd8b71e5d..0428f08138 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -12,6 +12,7 @@ open Pp open Constr +open Context open Genarg open Stdarg open Tacarg @@ -674,7 +675,7 @@ let hResolve id c occ t = let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) + (change_concl (mkLetIn (make_annot Name.Anonymous Sorts.Relevant,t_constr,t_constr_type,concl))) end let hResolve_auto id c t = diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 5e3f4df192..e188971f00 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1158,7 +1158,7 @@ let pr_goal_selector ~toplevel s = if n=0 then (List.rev acc, EConstr.of_constr ty) else match Constr.kind ty with | Constr.Prod(na,a,b) -> - strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b + strip_ty (([CAst.make na.Context.binder_name],EConstr.of_constr a)::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e78d0f93a4..b1d5c0252f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -15,6 +15,7 @@ open Names open Nameops open Namegen open Constr +open Context open EConstr open Vars open Reduction @@ -220,23 +221,23 @@ end) = struct let rec aux env evars ty l = let t = Reductionops.whd_all env (goalevars evars) ty in match EConstr.kind (goalevars evars) t, l with - | Prod (na, ty, b), obj :: cstrs -> + | Prod (na, ty, b), obj :: cstrs -> let b = Reductionops.nf_betaiota env (goalevars evars) b in - if noccurn (goalevars evars) 1 b (* non-dependent product *) then + if noccurn (goalevars evars) 1 b (* non-dependent product *) then let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in let evars, relty = mk_relty evars env ty obj in let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in - evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs + evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs else let (evars, b, arg, cstrs) = - aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs + aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs in let ty = Reductionops.nf_betaiota env (goalevars evars) ty in - let pred = mkLambda (na, ty, b) in - let liftarg = mkLambda (na, ty, arg) in - let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in - if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs + let pred = mkLambda (na, ty, b) in + let liftarg = mkLambda (na, ty, arg) in + let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in + if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.") | _, [] -> @@ -253,7 +254,7 @@ end) = struct let unfold_impl sigma t = match EConstr.kind sigma t with | App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) -> - mkProd (Anonymous, a, lift 1 b) + mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b) | _ -> assert false let unfold_all sigma t = @@ -279,7 +280,7 @@ end) = struct (app_poly env evd arrow [| a; b |]), unfold_impl (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) (app_poly env evd arrow [| a; b |]), unfold_impl @@ -308,7 +309,8 @@ end) = struct app_poly env evd pointwise_relation [| t; lift (-1) car; lift (-1) rel |] else app_poly env evd forall_relation - [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |] + [| t; mkLambda (make_annot n Sorts.Relevant, t, car); + mkLambda (make_annot n Sorts.Relevant, t, rel) |] let lift_cstr env evars (args : constr list) c ty cstr = let start evars env car = @@ -323,15 +325,15 @@ end) = struct else let sigma = goalevars evars in match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with - | Prod (na, ty, b) -> + | Prod (na, ty, b) -> if noccurn sigma 1 b then let b' = lift (-1) b in let evars, rb = aux evars env b' (pred n) in app_poly env evars pointwise_relation [| ty; b'; rb |] else - let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in + let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in app_poly env evars forall_relation - [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |] + [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |] | _ -> raise Not_found in let rec find env c ty = function @@ -481,8 +483,9 @@ let rec decompose_app_rel env evd t = | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in let ty = Typing.unsafe_type_of env evd argl in - let f'' = mkLambda (Name default_dependent_ident, ty, - mkLambda (Name (Id.of_string "y"), lift 1 ty, + let r = Retyping.relevance_of_type env evd ty in + let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty, + mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) in (f'', argl, argr) | App (f, args) -> @@ -522,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) = | Some c -> c | None -> let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with + match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.") @@ -803,7 +806,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation in EConstr.push_named - (LocalDef (Id.of_string "do_subrelation", + (LocalDef (make_annot (Id.of_string "do_subrelation") Sorts.Relevant, snd (app_poly_sort b env evars dosub [||]), snd (app_poly_nocheck env evars appsub [||]))) env @@ -906,7 +909,7 @@ let make_leibniz_proof env c ty r = let prf = e_app_poly env evars coq_f_equal [| r.rew_car; ty; - mkLambda (Anonymous, r.rew_car, c); + mkLambda (make_annot Anonymous Sorts.Relevant, r.rew_car, c); r.rew_from; r.rew_to; prf |] in RewPrf (rel, prf) | RewCast k -> r.rew_prf @@ -1103,7 +1106,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* else *) | Prod (n, dom, codom) -> - let lam = mkLambda (n, dom, codom) in + let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = if eq_constr (fst evars) ty mkProp then (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all @@ -1149,9 +1152,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n in + let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in let open Context.Rel.Declaration in - let env' = EConstr.push_rel (LocalAssum (n', t)) env in + let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in let state, b' = s.strategy { state ; env = env' ; unfresh ; @@ -1166,15 +1169,15 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let point = if prop then PropGlobal.pointwise_or_dep_relation else TypeGlobal.pointwise_or_dep_relation in - let evars, rel = point env r.rew_evars n' t r.rew_car rel in - let prf = mkLambda (n', t, prf) in + let evars, rel = point env r.rew_evars n'.binder_name t r.rew_car rel in + let prf = mkLambda (n', t, prf) in { r with rew_prf = RewPrf (rel, prf); rew_evars = evars } | x -> r in Success { r with - rew_car = mkProd (n, t, r.rew_car); - rew_from = mkLambda(n, t, r.rew_from); - rew_to = mkLambda (n, t, r.rew_to) } + rew_car = mkProd (n, t, r.rew_car); + rew_from = mkLambda(n, t, r.rew_from); + rew_to = mkLambda (n, t, r.rew_to) } | Fail | Identity -> b' in state, res @@ -1516,7 +1519,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul | Some (t, ty) -> let t = Reductionops.nf_evar evars' t in let ty = Reductionops.nf_evar evars' ty in - mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |]) + mkApp (mkLambda (make_annot (Name (Id.of_string "lemma")) Sorts.Relevant, ty, p), [| t |]) in let proof = match is_hyp with | None -> term @@ -1542,7 +1545,8 @@ let assert_replacing id newt tac = let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in let nc = match before with | [] -> assert false - | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem + | d :: rem -> insert_dependent env sigma + (LocalAssum (make_annot (NamedDecl.get_id d) Sorts.Relevant, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~typecheck:true begin fun sigma -> @@ -1586,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (LocalAssum (id, newt)) <*> + convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> @@ -1905,7 +1909,7 @@ let build_morphism_signature env sigma m = let cstrs = let rec aux t = match EConstr.kind sigma t with - | Prod (na, a, b) -> + | Prod (na, a, b) -> None :: aux b | _ -> [] in aux t diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 026c00b849..fcab98c7e8 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,7 +199,8 @@ let id_of_name = function basename | Sort s -> begin - match ESorts.kind sigma s with + match ESorts.kind sigma s with + | Sorts.SProp -> Label.to_id (Label.make "SProp") | Sorts.Prop -> Label.to_id (Label.make "Prop") | Sorts.Set -> Label.to_id (Label.make "Set") | Sorts.Type _ -> Label.to_id (Label.make "Type") diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 54924f1644..2b5e496168 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -12,6 +12,7 @@ (lazy)match and (lazy)match goal. *) open Names +open Context open Tacexpr open Context.Named.Declaration @@ -299,8 +300,8 @@ module PatternMatching (E:StaticEnvironment) = struct | LocalDef (id,body,hyp) -> pattern_match_term false bodypat body () <*> pattern_match_term true typepat hyp () <*> - put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*> - return id + put_terms (id_map_try_add_name hypname (EConstr.mkVar id.binder_name) empty_term_subst) <*> + return id.binder_name | LocalAssum (id,hyp) -> fail (** [hyp_match pat hyps] dispatches to diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 19256e054d..4c65445b89 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -142,7 +142,7 @@ let flatten_contravariant_conj _ ist = ~onlybinary:flags.binary_mode typ with | Some (_,args) -> - let newtyp = List.fold_right mkArrow args c in + let newtyp = List.fold_right (fun a b -> mkArrow a Sorts.Relevant b) args c in let intros = tclMAP (fun _ -> intro) args in let by = tclTHENLIST [intros; apply hyp; split; assumption] in tclTHENLIST [assert_ ~by newtyp; clear (destVar sigma hyp)] @@ -173,7 +173,7 @@ let flatten_contravariant_disj _ ist = typ with | Some (_,args) -> let map i arg = - let typ = mkArrow arg c in + let typ = mkArrow arg Sorts.Relevant c in let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in let by = tclTHENLIST [intro; apply hyp; ci; assumption] in assert_ ~by typ diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7adae148bd..ac34faa7da 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -23,6 +23,7 @@ open Names open Goptions open Mutils open Constr +open Context open Tactypes (** @@ -1243,7 +1244,7 @@ let dump_rexpr = lazy let prodn n env b = let rec prodrec = function | (0, env, b) -> b - | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (v,t,b)) + | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (make_annot v Sorts.Relevant,t,b)) | _ -> assert false in prodrec (n,env,b) @@ -1293,8 +1294,8 @@ let make_goal_of_formula sigma dexpr form = | FF -> Lazy.force coq_False | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) - | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False) + | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (xdump (pi+1) (xi+1) y) + | N(x) -> EConstr.mkArrow (xdump pi xi x) Sorts.Relevant (Lazy.force coq_False) | A(x,_,_) -> dump_cstr xi x | X(t) -> let idx = Env.get_rank props sigma t in EConstr.mkRel (pi+idx) in @@ -1327,7 +1328,7 @@ let make_goal_of_formula sigma dexpr form = | (e::l) -> let (name,expr,typ) = e in xset (EConstr.mkNamedLetIn - (Names.Id.of_string name) + (make_annot (Names.Id.of_string name) Sorts.Relevant) expr typ acc) l in xset concl l @@ -1614,7 +1615,7 @@ let abstract_formula hyps f = | I(f1,hyp,f2) -> (match xabs f1 , hyp, xabs f2 with | X a1 , Some _ , af2 -> af2 - | X a1 , None , X a2 -> X (EConstr.mkArrow a1 a2) + | X a1 , None , X a2 -> X (EConstr.mkArrow a1 Sorts.Relevant a2) | af1 , _ , af2 -> I(af1,hyp,af2) ) | FF -> FF diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index dff25b3a42..4802608fda 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -19,6 +19,7 @@ open CErrors open Util open Names open Constr +open Context open Nameops open EConstr open Tacticals.New @@ -431,8 +432,8 @@ let destructurate_prop sigma t = | Ind (isp,_), args -> Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id - | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) - | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") + | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body) + | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") | _ -> Kufo let nf = Tacred.simpl @@ -499,13 +500,13 @@ let context sigma operation path (t : constr) = | (p, Fix ((_,n as ln),(tys,lna,v))) -> let l = Array.length v in let v' = Array.copy v in - v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) + v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) | ((P_TYPE :: p), Prod (n,t,c)) -> - (mkProd (n,loop i p t,c)) + (mkProd (n,loop i p t,c)) | ((P_TYPE :: p), Lambda (n,t,c)) -> - (mkLambda (n,loop i p t,c)) + (mkLambda (n,loop i p t,c)) | ((P_TYPE :: p), LetIn (n,b,t,c)) -> - (mkLetIn (n,b,loop i p t,c)) + (mkLetIn (n,b,loop i p t,c)) | (p, _) -> failwith ("abstract_path " ^ string_of_int(List.length p)) in @@ -528,7 +529,7 @@ let occurrence sigma path (t : constr) = let abstract_path sigma typ path t = let term_occur = ref (mkRel 0) in let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in - mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur + mkLambda (make_annot (Name (Id.of_string "x")) Sorts.Relevant, typ, abstract), !term_occur let focused_simpl path = let open Tacmach.New in @@ -604,10 +605,10 @@ let clever_rewrite_base_poly typ p result theorem = let t = applist (mkLambda - (Name (Id.of_string "P"), - mkArrow typ mkProp, + (make_annot (Name (Id.of_string "P")) Sorts.Relevant, + mkArrow typ Sorts.Relevant mkProp, mkLambda - (Name (Id.of_string "H"), + (make_annot (Name (Id.of_string "H")) Sorts.Relevant, applist (mkRel 1,[result]), mkApp (Lazy.force coq_eq_ind_r, [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), @@ -1264,7 +1265,7 @@ let replay_history tactic_normalisation = mkApp (Lazy.force coq_ex, [| Lazy.force coq_Z; mkLambda - (Name vid, + (make_annot (Name vid) Sorts.Relevant, Lazy.force coq_Z, mk_eq (mkRel 1) eq1) |]) in @@ -1725,11 +1726,11 @@ let destructure_hyps = try match destructurate_type env sigma typ with | Kapp(Nat,_) | Kapp(Z,_) -> - let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in - let hty = mk_gen_eq typ (mkVar i) body in + let hid = fresh_id Id.Set.empty (add_suffix i.binder_name "_eqn") gl in + let hty = mk_gen_eq typ (mkVar i.binder_name) body in tclTHEN (assert_by (Name hid) hty reflexivity) - (loop (LocalAssum (hid, hty) :: lit)) + (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit)) | _ -> loop lit with e when catchable_exception e -> loop lit end @@ -1742,18 +1743,20 @@ let destructure_hyps = | Kapp(Or,[t1;t2]) -> (tclTHENS (elim_id i) - [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); - onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) + [ onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t1)::lit))); + onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) + loop (LocalAssum (make_annot i1 Sorts.Relevant,t1) :: + LocalAssum (make_annot i2 Sorts.Relevant,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) + loop (LocalAssum (make_annot i1 Sorts.Relevant,mkArrow t1 Sorts.Relevant t2) :: + LocalAssum (make_annot i2 Sorts.Relevant,mkArrow t2 Sorts.Relevant t1) :: lit))) | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) @@ -1764,7 +1767,7 @@ let destructure_hyps = (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) t2) :: lit)))) ] else loop lit @@ -1775,7 +1778,7 @@ let destructure_hyps = (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in @@ -1784,7 +1787,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_or (mk_not t1) (mk_not t2)) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) (mk_not t2)) :: lit)))) ] | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in @@ -1794,7 +1797,7 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i, mk_or (mk_and t1 (mk_not t2)) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_and t1 (mk_not t2)) (mk_and (mk_not t1) t2)) :: lit)))) ] | Kimp(t1,t2) -> @@ -1806,14 +1809,14 @@ let destructure_hyps = [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> - (loop (LocalAssum (i,mk_and t1 (mk_not t2)) :: lit)))) + (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and t1 (mk_not t2)) :: lit)))) ] | Kapp(Not,[t]) -> let d = decidability t in tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) + (onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t) :: lit)))) ] | Kapp(op,[t1;t2]) -> (try diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index a6b6c57ff9..89528fe357 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -16,6 +16,7 @@ open CErrors open Util open Term open Constr +open Context open Proof_search open Context.Named.Declaration @@ -127,7 +128,7 @@ let rec make_hyps env sigma atom_env lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps env sigma atom_env (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id.binder_name c) lenv || (Retyping.get_sort_family_of env sigma typ != InProp) then hrec @@ -291,7 +292,7 @@ let rtauto_tac = build_form formula; build_proof [] 0 prf|]) in let term= - applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in + applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in let build_end_time=System.get_time () in let () = if !verbose then begin diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 49b5ee5ac7..3de0ba44df 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -23,6 +23,6 @@ val make_hyps -> atom_env -> EConstr.types list -> EConstr.named_context - -> (Names.Id.t * Proof_search.form) list + -> (Names.Id.t Context.binder_annot * Proof_search.form) list val rtauto_tac : unit Proofview.tactic diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 0961edb6cb..58daa7a7d4 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -15,6 +15,7 @@ open Names open Evd open Term open Constr +open Context open Termops open Printer open Locusops @@ -429,15 +430,16 @@ let convert_concl t = Tactics.convert_concl t DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with - | Prod(_,src,tgt) -> - Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl + | Prod(x,src,tgt) -> + let x = {x with binder_name = !orig_name_ref} in + Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (x,src,tgt))) gl | _ -> CErrors.anomaly (str "gentac creates no product") (* Reduction that preserves the Prod/Let spine of the "in" tactical. *) let inc_safe n = if n = 0 then n else n + 1 let rec safe_depth s c = match EConstr.kind s c with -| LetIn (Name x, _, _, c') when is_discharged_id x -> safe_depth s c' + 1 +| LetIn ({binder_name=Name x}, _, _, c') when is_discharged_id x -> safe_depth s c' + 1 | LetIn (_, _, _, c') | Prod (_, _, c') -> inc_safe (safe_depth s c') | _ -> 0 @@ -529,7 +531,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) = let concl = EConstr.Unsafe.to_constr evi.evar_concl in let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function - | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) + | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t x.binder_relevance c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma t in @@ -552,7 +554,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) = | _ -> Constr.map_with_binders ((+) 1) get i c in let rec loop c i = function | (_, (n, t)) :: evl -> - loop (mkLambda (mk_evar_name n, get (i - 1) t, c)) (i - 1) evl + loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, get (i - 1) t, c)) (i - 1) evl | [] -> c in List.length evlist, EConstr.of_constr (loop (get 1 c0) 1 evlist), List.map fst evlist, ucst @@ -590,7 +592,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let concl = EConstr.Unsafe.to_constr evi.evar_concl in let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function - | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) + | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t x.binder_relevance c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma0 (nf_evar sigma t) in @@ -646,7 +648,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in - loopP evlist (mkProd (n, t, c)) (i - 1) evl + loopP evlist (mkProd (make_annot n Sorts.Relevant, t, c)) (i - 1) evl | [] -> c in let rec loop c i = function | (_, (n, t, _)) :: evl -> @@ -658,7 +660,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = List.map (fun (k,_) -> mkRel (fst (lookup k i evlist))) (List.rev t_evplist) in let c = if extra_args = [] then c else app extra_args 1 c in - loop (mkLambda (mk_evar_name n, t, c)) (i - 1) evl + loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, t, c)) (i - 1) evl | [] -> c in let res = loop (get evlist 1 c0) 1 evlist in pp(lazy(str"res= " ++ pr_constr res)); @@ -679,6 +681,9 @@ let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t) let pfe_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty +let pfe_type_relevance_of gl t = + let gl, ty = pfe_type_of gl t in + gl, ty, pf_apply Retyping.relevance_of_term gl t let pf_type_of gl t = let sigma, ty = pf_type_of gl (EConstr.of_constr t) in re_sig (sig_it gl) sigma, EConstr.Unsafe.to_constr ty @@ -710,13 +715,13 @@ let pf_abs_cterm gl n c0 = | _ -> [], strip i c in let rec strip_evars i c = match Constr.kind c with | Lambda (x, t1, c1) when i < n -> - let na = nb_evar_deps x in + let na = nb_evar_deps x.binder_name in let dl, t2 = strip_ndeps (i + na) i t1 in let na' = List.length dl in eva.(i) <- Array.of_list (na - na' :: dl); let x' = if na' = 0 then Name (pf_type_id gl (EConstr.of_constr t2)) else mk_evar_name na' in - mkLambda (x', t2, strip_evars (i + 1) c1) + mkLambda ({x with binder_name=x'}, t2, strip_evars (i + 1) c1) (* if noccurn 1 c2 then lift (-1) c2 else mkLambda (Name (pf_type_id gl t2), t2, c2) *) | _ -> strip i c in @@ -739,9 +744,9 @@ let rec constr_name sigma c = match EConstr.kind sigma c with | _ -> Anonymous let pf_mkprod gl c ?(name=constr_name (project gl) c) cl = - let gl, t = pfe_type_of gl c in - if name <> Anonymous || EConstr.Vars.noccurn (project gl) 1 cl then gl, EConstr.mkProd (name, t, cl) else - gl, EConstr.mkProd (Name (pf_type_id gl t), t, cl) + let gl, t, r = pfe_type_relevance_of gl c in + if name <> Anonymous || EConstr.Vars.noccurn (project gl) 1 cl then gl, EConstr.mkProd (make_annot name r, t, cl) else + gl, EConstr.mkProd (make_annot (Name (pf_type_id gl t)) r, t, cl) let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project gl) c cl) @@ -783,13 +788,17 @@ let mkRefl t c gl = let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in - match pf_get_hyp gl id, mode with - | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl'))) + let decl = pf_get_hyp gl id in + match decl, mode with + | NamedDecl.LocalAssum _, _ | NamedDecl.LocalDef _, "(" -> + let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true + (EConstr.of_constr (mkProd (id', NamedDecl.get_type decl, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> + let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in Proofview.V82.of_tactic - (convert_concl (EConstr.of_constr (mkLetIn (Name id', v, t, cl')))) gl + (convert_concl (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl (* wildcard names *) let clear_wilds wilds gl = @@ -983,7 +992,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = let rec loop sigma bo args = function (* saturate with metas *) | 0 -> EConstr.mkApp (t, Array.of_list (List.rev args)), re_sig si sigma | n -> match EConstr.kind sigma bo with - | Lambda (_, ty, bo) -> + | Lambda (_, ty, bo) -> if not (EConstr.Vars.closed0 sigma ty) then raise dependent_apply_error; let m = Evarutil.new_meta () in @@ -1019,7 +1028,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;; let rec fst_prod red tac = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in match EConstr.kind (Proofview.Goal.sigma gl) concl with - | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id + | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id.binder_name | _ -> if red then Tacticals.New.tclZEROMSG (str"No product even after head-reduction.") else Tacticals.New.tclTHEN Tactics.hnf_in_concl (fst_prod true tac) end @@ -1122,14 +1131,14 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = errorstrm (str "@ can be used with variables only") else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with | NamedDecl.LocalAssum _ -> errorstrm (str "@ can be used with let-ins only") - | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (Name name,b,ty,cl),c,clr,ucst,gl + | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl),c,clr,ucst,gl else let gl, ccl = pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl else if to_ind && occ = None then let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in let ucst = UState.union ucst ucst' in if nv = 0 then anomaly "occur_existential but no evars" else - let gl, pty = pfe_type_of gl p in - false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl + let gl, pty, rp = pfe_type_relevance_of gl p in + false, pat, EConstr.mkProd (make_annot (constr_name (project gl) c) rp, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs) @@ -1235,7 +1244,10 @@ let abs_wgen keep_let f gen (gl,args,c) = (EConstr.Vars.subst_var x c) | _, Some ((x, _), None) -> let x = hoi_id x in - gl, EConstr.mkVar x :: args, EConstr.mkProd (Name (f x),Tacmach.pf_get_hyp_typ gl x, EConstr.Vars.subst_var x c) + let hyp = Tacmach.pf_get_hyp gl x in + let x' = make_annot (Name (f x)) (NamedDecl.get_relevance hyp) in + let prod = EConstr.mkProd (x', NamedDecl.get_type hyp, EConstr.Vars.subst_var x c) in + gl, EConstr.mkVar x :: args, prod | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in @@ -1246,8 +1258,8 @@ let abs_wgen keep_let f gen (gl,args,c) = let t = EConstr.of_constr t in evar_closed t p; let ut = red_product_skip_id env sigma t in - let gl, ty = pfe_type_of gl t in - pf_merge_uc ucst gl, args, EConstr.mkLetIn(Name (f x), ut, ty, c) + let gl, ty, r = pfe_type_relevance_of gl t in + pf_merge_uc ucst gl, args, EConstr.mkLetIn(make_annot (Name (f x)) r, ut, ty, c) | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in @@ -1257,8 +1269,8 @@ let abs_wgen keep_let f gen (gl,args,c) = let c = EConstr.of_constr c in let t = EConstr.of_constr t in evar_closed t p; - let gl, ty = pfe_type_of gl t in - pf_merge_uc ucst gl, t :: args, EConstr.mkProd(Name (f x), ty, c) + let gl, ty, r = pfe_type_relevance_of gl t in + pf_merge_uc ucst gl, t :: args, EConstr.mkProd(make_annot (Name (f x)) r, ty, c) | _ -> gl, args, c let clr_of_wgen gen clrs = match gen with @@ -1321,8 +1333,8 @@ let unsafe_intro env decl b = end let set_decl_id id = let open Context in function - | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum(id,ty) - | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef(id,ty,t) + | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum({name with binder_name=id},ty) + | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef({name with binder_name=id},ty,t) let rec decompose_assum env sigma orig_goal = let open Context in @@ -1400,8 +1412,8 @@ let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with - | Prod(_,src,tgt) -> - convert_concl_no_check EConstr.(mkProd (name,src,tgt)) + | Prod(x,src,tgt) -> + convert_concl_no_check EConstr.(mkProd ({x with binder_name = name},src,tgt)) | _ -> CErrors.anomaly (Pp.str "rename_hd_prod: no head product") end @@ -1429,11 +1441,12 @@ let tacMKPROD c ?name cl = tacCONSTR_NAME ?name c >>= fun name -> Goal.enter_one ~__LOC__ begin fun g -> let sigma, env = Goal.sigma g, Goal.env g in + let r = Retyping.relevance_of_term env sigma c in if name <> Names.Name.Anonymous || EConstr.Vars.noccurn sigma 1 cl - then tclUNIT (EConstr.mkProd (name, t, cl)) + then tclUNIT (EConstr.mkProd (make_annot name r, t, cl)) else let name = Names.Id.of_string (Namegen.hdchar env sigma t) in - tclUNIT (EConstr.mkProd (Names.Name.Name name, t, cl)) + tclUNIT (EConstr.mkProd (make_annot (Name.Name name) r, t, cl)) end let tacINTERP_CPATTERN cp = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e642b5e788..9662daa7c7 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -155,7 +155,7 @@ val pf_e_type_of : val splay_open_constr : Goal.goal Evd.sigma -> evar_map * EConstr.t -> - (Names.Name.t * EConstr.t) list * EConstr.t + (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool val mk_term : ssrtermkind -> constr_expr -> ssrterm @@ -205,6 +205,9 @@ val pf_type_of : val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types +val pfe_type_relevance_of : + Goal.goal Evd.sigma -> + EConstr.t -> Goal.goal Evd.sigma * EConstr.types * Sorts.relevance val pf_abs_prod : Name.t -> Goal.goal Evd.sigma -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 7216849948..82a88678f0 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -15,6 +15,7 @@ open Names open Printer open Term open Constr +open Context open Termops open Tactypes open Tacmach @@ -364,14 +365,14 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let gl, eq = get_eq_type gl in let gen_eq_tac, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in - let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in + let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 (pf_concl orig_gl)) in let new_concl = fire_subst gl new_concl in let erefl, gl = mkRefl t c gl in let erefl = fire_subst gl erefl in apply_type new_concl [erefl], gl in let rel = k + if c_is_head_p then 1 else 0 in let src, gl = mkProt EConstr.mkProp EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in - let concl = EConstr.mkArrow src (EConstr.Vars.lift 1 concl) in + let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in let clr = if deps <> [] then clr else [] in concl, gen_eq_tac, clr, gl | _ -> concl, Tacticals.tclIDTAC, clr, gl in @@ -446,7 +447,7 @@ let injecteq_id = mk_internal_id "injection equation" let revtoptac n0 gl = let n = pf_nb_prod gl - n0 in let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in - let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in + let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl @@ -486,7 +487,7 @@ let perform_injection c gl = CErrors.user_err (Pp.str "can't decompose a quantified equality") else let cl = pf_concl gl in let n = List.length dc in let c_eq = mkEtaApp c n 2 in - let cl1 = EConstr.mkLambda EConstr.(Anonymous, mkArrow eqt cl, mkApp (mkRel 1, [|c_eq|])) in + let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in let id = injecteq_id in let id_with_ebind = (EConstr.mkVar id, NoBindings) in let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 64e023c68a..18461c0533 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -15,6 +15,7 @@ open Util open Names open Term open Constr +open Context open Vars open Locus open Printer @@ -136,7 +137,7 @@ let newssrcongrtac arg ist gl = (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) (fun () -> let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in - let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in + let arrow = EConstr.mkArrow lhs Sorts.Relevant (EConstr.Vars.lift 1 rhs) in tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|]) (fun lr -> tclTHEN (Proofview.V82.of_tactic (Tactics.apply (ssr_congr lr))) (congrtac (arg, mkRType) ist)) (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow"))) @@ -335,7 +336,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in (sigma, ev) in - let pred = EConstr.mkNamedLambda pattern_id rdx_ty pred in + let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in @@ -362,7 +363,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let names = let rec aux t = function 0 -> [] | n -> let t = Reductionops.whd_all env sigma t in match EConstr.kind_of_type sigma t with - | ProdType (name, _, t) -> name :: aux t (n-1) + | ProdType (name, _, t) -> name.binder_name :: aux t (n-1) | _ -> assert false in aux hd_ty (Array.length args) in hd_ty, Util.List.map_filter (fun (t, name) -> let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in @@ -403,7 +404,7 @@ let rwcltac cl rdx dir sr gl = let new_rdx = if dir = L2R then a.(2) else a.(1) in pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl | _ -> - let cl' = EConstr.mkApp (EConstr.mkNamedLambda pattern_id rdxt cl, [|rdx|]) in + let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl @@ -413,8 +414,8 @@ let rwcltac cl rdx dir sr gl = try EConstr.destCast (project gl) r2 with _ -> errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr)) ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in - let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in - let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in + let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in + let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in @@ -426,7 +427,9 @@ let rwcltac cl rdx dir sr gl = if occur_existential (project gl) (Tacmach.pf_concl gl) then errorstrm Pp.(str "Rewriting impacts evars") else errorstrm Pp.(str "Dependent type error in rewrite of " - ++ pr_constr_env (pf_env gl) (project gl) (Term.mkNamedLambda pattern_id (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) + ++ pr_constr_env (pf_env gl) (project gl) + (Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant) + (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) in tclTHEN cvtac' rwtac gl diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 8c1363020a..9ea35b8694 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -13,6 +13,7 @@ open Pp open Names open Constr +open Context open Tacmach open Ssrmatching_plugin.Ssrmatching @@ -54,7 +55,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = let c, (gl, cty) = match EConstr.kind sigma c with | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in - let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in + let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl open Util @@ -162,7 +163,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in + pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function @@ -190,10 +191,10 @@ let havetac ist Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl)) | _,true,true -> let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in - gl, EConstr.mkArrow ty concl, hint, itac, clr + gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, itac, clr | _,false,true -> let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in - gl, EConstr.mkArrow ty concl, hint, id, itac_c + gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, id, itac_c | _, false, false -> let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac @@ -233,7 +234,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let gens = List.filter (function _, Some _ -> true | _ -> false) gens in let concl = pf_concl gl in let c = EConstr.mkProp in - let c = if cut_implies_goal then EConstr.mkArrow c concl else c in + let c = if cut_implies_goal then EConstr.mkArrow c Sorts.Relevant concl else c in let gl, args, c = List.fold_right mkabs gens (gl,[],c) in let env, _ = List.fold_left (fun (env, c) _ -> @@ -245,10 +246,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let fake_gl = {Evd.it = k; Evd.sigma = sigma} in let _, ct, _, uc = pf_interp_ty ist fake_gl ct in let rec var2rel c g s = match EConstr.kind sigma c, g with - | Prod(Anonymous,_,c), [] -> EConstr.mkProd(Anonymous, EConstr.Vars.subst_vars s ct, c) + | Prod({binder_name=Anonymous} as x,_,c), [] -> EConstr.mkProd(x, EConstr.Vars.subst_vars s ct, c) | Sort _, [] -> EConstr.Vars.subst_vars s ct - | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) - | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) + | LetIn({binder_name=Name id} as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) + | Prod({binder_name=Name id} as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in let c = var2rel c gens [] in let rec pired c = function diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index a8dfd69240..e9fe1f3e48 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -13,6 +13,7 @@ open Ssrmatching_plugin open Util open Names open Constr +open Context open Proofview open Proofview.Notations @@ -393,12 +394,12 @@ let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> let sigma, m = Evarutil.new_evar env sigma abstract_ty in sigma, (m, abstract_ty) in let sigma, kont = - let rd = Context.Rel.Declaration.LocalAssum (Name id, abstract_ty) in + let rd = Context.Rel.Declaration.LocalAssum (make_annot (Name id) Sorts.Relevant, abstract_ty) in let sigma, ev = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in sigma, ev in let term = - EConstr.(mkApp (mkLambda(Name id,abstract_ty,kont),[|abstract_proof|])) in + EConstr.(mkApp (mkLambda(make_annot (Name id) Sorts.Relevant,abstract_ty,kont),[|abstract_proof|])) in let sigma, _ = Typing.type_of env sigma term in sigma, term end in @@ -608,7 +609,7 @@ let with_defective maintac deps clr = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in let top_id = match EConstr.kind_of_type sigma concl with - | Term.ProdType (Name id, _, _) + | Term.ProdType ({binder_name=Name id}, _, _) when Ssrcommon.is_discharged_id id -> id | _ -> Ssrcommon.top_id in let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in @@ -683,7 +684,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr = let name = Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in let new_concl = - mkProd (Name name, case_ty, mkArrow refl (Vars.lift 2 concl)) in + mkProd (make_annot (Name name) Sorts.Relevant, case_ty, mkArrow refl Sorts.Relevant (Vars.lift 2 concl)) in let erefl, sigma = mkCoqRefl case_ty case env sigma in Proofview.Unsafe.tclEVARS sigma <*> Tactics.apply_type ~typecheck:true new_concl [case;erefl] @@ -707,7 +708,7 @@ let mkEq dir cl c t n env sigma = eqargs.(Ssrequality.dir_org dir) <- mkRel n; let eq, sigma = mkCoqEq env sigma in let refl, sigma = mkCoqRefl t c env sigma in - mkArrow (mkApp (eq, eqargs)) (Vars.lift 1 cl), refl, sigma + mkArrow (mkApp (eq, eqargs)) Sorts.Relevant (Vars.lift 1 cl), refl, sigma (** in [tac/v: last gens..] the first (last to be run) generalization is "special" in that is it also the main argument of [tac] and is eventually @@ -743,7 +744,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only") | Context.Named.Declaration.LocalDef (name, b, ty) -> Unsafe.tclEVARS sigma <*> - tclUNIT (true, EConstr.mkLetIn (Name name,b,ty,cl), c, clr) + tclUNIT (true, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl), c, clr) else Unsafe.tclEVARS sigma <*> Ssrcommon.tacMKPROD c cl >>= fun ccl -> @@ -757,7 +758,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin Unsafe.tclEVARS sigma <*> Ssrcommon.tacTYPEOF p >>= fun pty -> (* TODO: check bug: cl0 no lift? *) - let ccl = EConstr.mkProd (Ssrcommon.constr_name sigma c, pty, cl0) in + let ccl = EConstr.mkProd (make_annot (Ssrcommon.constr_name sigma c) Sorts.Relevant, pty, cl0) in tclUNIT (false, ccl, p, clr) else Ssrcommon.errorstrm Pp.(str "generalized term didn't match") diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index f12f9fac0f..bbe7bde78b 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -12,6 +12,7 @@ open Names open Constr +open Context open Termops open Tacmach @@ -102,10 +103,10 @@ let endclausestac id_map clseq gl_id cl0 gl = forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in let rec unmark c = match EConstr.kind (project gl) c with | Var id when hidden_clseq clseq && id = gl_id -> cl0 - | Prod (Name id, t, c') when List.mem_assoc id id_map -> - EConstr.mkProd (Name (orig_id id), unmark t, unmark c') - | LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> - EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c') + | Prod ({binder_name=Name id} as na, t, c') when List.mem_assoc id id_map -> + EConstr.mkProd ({na with binder_name=Name (orig_id id)}, unmark t, unmark c') + | LetIn ({binder_name=Name id} as na, v, t, c') when List.mem_assoc id id_map -> + EConstr.mkLetIn ({na with binder_name=Name (orig_id id)}, unmark v, unmark t, unmark c') | _ -> EConstr.map (project gl) unmark c in let utac hyp = Proofview.V82.of_tactic diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 2794696017..537fd7d7b4 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -10,6 +10,7 @@ open Util open Names +open Context open Ltac_plugin @@ -95,7 +96,7 @@ let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl -> let concl = Goal.concl gl in let id = (* We keep the orig name for checks in "in" tcl *) match EConstr.kind_of_type (Goal.sigma gl) concl with - | Term.ProdType(Name.Name id, _, _) + | Term.ProdType({binder_name=Name.Name id}, _, _) when Ssrcommon.is_discharged_id id -> id | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in let view = EConstr.mkVar id in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index fb99b87108..b83a6a34cb 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -16,6 +16,7 @@ open Pp open Genarg open Stdarg open Term +open Context module CoqConstr = Constr open CoqConstr open Vars @@ -383,7 +384,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = | Context.Named.Declaration.LocalDef (x, b, t) -> d, mkNamedLetIn x (put b) (put t) c | Context.Named.Declaration.LocalAssum (x, t) -> - mkVar x :: d, mkNamedProd x (put t) c in + mkVar x.binder_name :: d, mkNamedProd x (put t) c in let a, t = Context.Named.fold_inside abs_dc ~init:([], (put @@ EConstr.Unsafe.to_constr evi.evar_concl)) @@ -548,7 +549,7 @@ let match_upats_FO upats env sigma0 ise orig_c = if skip || not (closed0 c') then () else try let _ = match u.up_k with | KpatFlex -> - let kludge v = mkLambda (Anonymous, mkProp, v) in + let kludge v = mkLambda (make_annot Anonymous Sorts.Relevant, mkProp, v) in unif_FO env ise (kludge u.up_FO) (kludge c') | KpatLet -> let kludge vla = @@ -1286,7 +1287,7 @@ let ssrpatterntac _ist arg gl = let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in - let concl = EConstr.mkLetIn (Name (Id.of_string "selected"), t, tty, concl_x) in + let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) |