diff options
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 16 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 10 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 85 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 17 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 12 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 16 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 31 |
8 files changed, 107 insertions, 82 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bd5fb1d92..29e824f44 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g *) +let pr_leconstr_fp = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let debug_queue = Stack.create () let rec print_debug_queue e = @@ -172,7 +176,7 @@ let is_incompatible_eq sigma t = | _ -> false with e when CErrors.noncritical e -> false in - if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t); + if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t); res let change_hyp_with_using msg hyp_id t tac : tactic = @@ -220,7 +224,8 @@ let find_rectype env sigma c = let isAppConstruct ?(env=Global.env ()) sigma t = try let t',l = find_rectype env sigma t in - observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l))); + observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++ + Printer.pr_leconstr_env env sigma (applist (t',l))); true with Not_found -> false @@ -233,7 +238,8 @@ exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin - observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t ); + observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++ + match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t ); raise NoChange; end in @@ -841,7 +847,7 @@ let build_proof | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam princ_params ); observe (str "fbody_with_full_params := " ++ - pr_leconstr fbody_with_full_params + pr_leconstr_env (Global.env ()) !evd fbody_with_full_params ); let all_funs_with_full_params = Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 722dbc16b..3899bc709 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -115,7 +115,9 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in - observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); + observe (str "replacing " ++ + pr_lconstr_env env Evd.empty c ++ str " by " ++ + pr_lconstr_env env Evd.empty res); res in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = @@ -565,7 +567,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ List.map (* we can now compute the other principles *) (fun scheme_type -> incr i; - observe (Printer.pr_lconstr scheme_type); + observe (Printer.pr_lconstr_env env sigma scheme_type); let type_concl = (strip_prod_assum scheme_type) in let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in let f = fst (decompose_app applied_f) in @@ -577,8 +579,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let g = fst (decompose_app applied_g) in if Constr.equal f g then raise (Found_type j); - observe (Printer.pr_lconstr f ++ str " <> " ++ - Printer.pr_lconstr g) + observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++ + Printer.pr_lconstr_env env sigma g) ) ta; diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8ab6dbcdf..d04b7a33d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -379,29 +379,30 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let open Context.Rel.Declaration in - match decl with + 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) -> - let new_t = substl ctxt t in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr 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) -> - let new_t = substl ctxt t in - let new_v = substl ctxt v in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ - str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) - ) + 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) -> + let new_t = substl ctxt t in + let new_v = substl ctxt v 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 () ++ + str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++ + 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.rel_context new_env) ~init:(env,[]) ) @@ -479,7 +480,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr rt); + observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> @@ -652,8 +653,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) [] in assert (Int.equal (Array.length case_pats) 2); @@ -684,8 +685,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); @@ -897,24 +898,24 @@ let same_raw_term rt1 rt2 = | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = - let rec decompose_raw_eq lhs rhs acc = - observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs); - let (rhd,lrhs) = glob_decompose_app rhs in - let (lhd,llhs) = glob_decompose_app lhs in - observe (str "lhd := " ++ pr_glob_constr lhd); - observe (str "rhd := " ++ pr_glob_constr rhd); + let _, env = Pfedit.get_current_context () in + let rec decompose_raw_eq lhs rhs acc = + observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); + let (rhd,lrhs) = glob_decompose_app rhs in + let (lhd,llhs) = glob_decompose_app lhs in + observe (str "lhd := " ++ pr_glob_constr_env env lhd); + observe (str "rhd := " ++ pr_glob_constr_env env rhd); observe (str "llhs := " ++ int (List.length llhs)); observe (str "lrhs := " ++ int (List.length lrhs)); - let sllhs = List.length llhs in - let slrhs = List.length lrhs in - if same_raw_term lhd rhd && Int.equal sllhs slrhs + let sllhs = List.length llhs in + let slrhs = List.length lrhs in + if same_raw_term lhd rhd && Int.equal sllhs slrhs then (* let _ = assert false in *) List.fold_right2 decompose_raw_eq llhs lrhs acc else (lhs,rhs)::acc in decompose_raw_eq lhs rhs [] - exception Continue (* @@ -923,7 +924,7 @@ exception Continue eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_glob_constr rt); + observe (str "rebuilding : " ++ pr_glob_constr_env env rt); let open Context.Rel.Declaration in let open CAst in match DAst.get rt with @@ -967,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try - observe (str "computing new type for eq : " ++ pr_glob_constr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when CErrors.noncritical e -> raise Continue @@ -1012,7 +1013,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let eq' = DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = @@ -1099,7 +1100,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = rebuild_cons env nb_args relname args crossed_types depth new_rt else raise Continue with Continue -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1115,7 +1116,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1134,7 +1135,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_glob_constr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index dab094f91..f01b6669d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -46,7 +46,7 @@ let functional_induction with_clean c princl pat = try find_Function_infos c' with Not_found -> user_err (str "Cannot find induction information on "++ - Printer.pr_leconstr (mkConst c') ) + Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with | InProp -> finfo.prop_lemma @@ -74,7 +74,7 @@ let functional_induction with_clean c princl pat = (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) user_err (str "Cannot find induction principle for " - ++Printer.pr_leconstr (mkConst c') ) + ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in let princ = EConstr.of_constr princ in (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') @@ -841,12 +841,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list * let make_graph (f_ref:global_reference) = let c,c_body = match f_ref with - | ConstRef c -> - begin try c,Global.lookup_constant c - with Not_found -> - raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) ) - end - | _ -> raise (UserError (None, str "Not a function reference") ) + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + let sigma, env = Pfedit.get_current_context () in + raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) + end + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 61d207b95..8bf6e48fd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -333,15 +333,17 @@ let discharge_Function (_,finfos) = } let pr_ocst c = - Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let sigma, env = Pfedit.get_current_context () in + Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) let pr_info f_info = + let sigma, env = Pfedit.get_current_context () in str "function_constant := " ++ - Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try - Printer.pr_lconstr - (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) + Printer.pr_lconstr_env env sigma + (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -349,7 +351,7 @@ let pr_info f_info = str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 692a874d3..694c80051 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -851,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma); + observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) funs_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b372241d2..9e2774ff3 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -90,20 +90,28 @@ let next_ident_fresh (id:Id.t) = (* comment this line to see debug msgs *) let msg x = () ;; let pr_lconstr c = str "" (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c) -let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prconstr c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c) + +let prconstrnl c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n") + let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) let prNamedConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} "); msg(str ""); end let prNamedRConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b8d41d539..04d729b10 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -54,6 +54,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] +let pr_leconstr_rd = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let coq_init_constant s = EConstr.of_constr ( Universes.constr_of_global @@ @@ -337,7 +341,8 @@ let check_not_nested sigma forbidden e = try check_not_nested e with UserError(_,p) -> - user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p) + let _, env = Pfedit.get_current_context () in + user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -455,7 +460,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + 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) -> begin @@ -463,7 +468,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + 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 | Case(ci,t,a,l) -> begin @@ -491,8 +496,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g - | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> @@ -515,7 +520,7 @@ and travel_args jinfo is_final continuation_tac infos = {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = observe_tac - (str jinfo.message ++ Printer.pr_leconstr expr_info.info) + (str jinfo.message ++ pr_leconstr_rd expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) @@ -731,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a') + observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS destruct_tac @@ -740,7 +745,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) )) g @@ -991,11 +996,11 @@ let rec intros_values_eq expr_info acc = let equation_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info) + observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos) + (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch @@ -1419,7 +1424,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1471,7 +1476,7 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in |