diff options
50 files changed, 282 insertions, 288 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8290ca945..04aacdc09 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -70,10 +70,10 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) (* term printers *) let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) -let ppconstr x = pp (Termops.print_constr x) -let ppeconstr x = pp (Termops.print_constr (EConstr.Unsafe.to_constr x)) +let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) +let ppeconstr x = pp (Termops.print_constr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) -let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x)) let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x @@ -98,9 +98,9 @@ let ppidmap pr l = pp (pridmap pr l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 - (Termops.print_constr c ++ + (Termops.print_constr (EConstr.of_constr c) ++ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ - Termops.print_constr c ++ str">") ++ + Termops.print_constr (EConstr.of_constr c) ++ str">") ++ (if id = id0 then mt () else spc () ++ str "<canonical: " ++ pr_id id ++ str ">")))) @@ -109,7 +109,7 @@ let ppididmap = ppidmap (fun _ -> pr_id) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") - ++ str "," ++ spc () ++ Termops.print_constr (EConstr.Unsafe.to_constr c)) + ++ str "," ++ spc () ++ Termops.print_constr c) let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) @@ -159,7 +159,7 @@ let prdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) -let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n) +let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n) let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) let pp_state_t n = pp (Reductionops.pr_state n) diff --git a/engine/evd.ml b/engine/evd.ml index d8a658e3e..9c05c6c02 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1265,7 +1265,7 @@ let protect f x = let (f_print_constr, print_constr_hook) = Hook.make () -let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a +let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) empty c) a let pr_meta_map mmap = let pr_name = function @@ -1423,11 +1423,11 @@ let pr_evar_constraints pbs = Namegen.make_all_name_different env in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - Hook.get f_print_constr env t1 ++ spc () ++ + Hook.get f_print_constr env empty t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ Hook.get f_print_constr env t2 + spc () ++ Hook.get f_print_constr env empty t2 in prlist_with_sep fnl pr_evconstr pbs diff --git a/engine/evd.mli b/engine/evd.mli index 5c9effd4b..4e8284675 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -607,7 +607,7 @@ val pr_evar_suggested_name : existential_key -> evar_map -> Id.t (** {5 Debug pretty-printers} *) -val print_constr_hook : (Environ.env -> constr -> Pp.std_ppcmds) Hook.t +val print_constr_hook : (Environ.env -> evar_map -> constr -> Pp.std_ppcmds) Hook.t val pr_evar_info : evar_info -> Pp.std_ppcmds val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds diff --git a/engine/termops.ml b/engine/termops.ml index 465832c10..46e9ad927 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -97,11 +97,11 @@ let rec pr_constr c = match kind_of_term c with cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") -let term_printer = ref (fun _ -> pr_constr) -let print_constr_env t = !term_printer t -let print_constr t = !term_printer (Global.env()) t +let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c)) +let print_constr_env env sigma t = !term_printer env sigma t +let print_constr t = !term_printer (Global.env()) Evd.empty t let set_print_constr f = term_printer := f -let () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c) +let () = Hook.set Evd.print_constr_hook (fun env sigma c -> !term_printer env sigma (EConstr.of_constr c)) let pr_var_decl env decl = let open NamedDecl in @@ -109,9 +109,10 @@ let pr_var_decl env decl = | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) - let pb = print_constr_env env c in + let c = EConstr.of_constr c in + let pb = print_constr_env env Evd.empty c in (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env (get_type decl) in + let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp)) @@ -121,9 +122,10 @@ let pr_rel_decl env decl = | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) - let pb = print_constr_env env c in + let c = EConstr.of_constr c in + let pb = print_constr_env env Evd.empty c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env (get_type decl) in + let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) diff --git a/engine/termops.mli b/engine/termops.mli index d7d9c743d..3f924cfa1 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -21,9 +21,9 @@ val pr_sort_family : sorts_family -> std_ppcmds val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds (** debug printer: do not use to display terms to the casual user... *) -val set_print_constr : (env -> Constr.constr -> std_ppcmds) -> unit -val print_constr : Constr.constr -> std_ppcmds -val print_constr_env : env -> Constr.constr -> std_ppcmds +val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit +val print_constr : constr -> std_ppcmds +val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds val print_named_context : env -> std_ppcmds val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds val print_rel_context : env -> std_ppcmds diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 3047d2bce..113fe40ba 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -11,6 +11,7 @@ open Loc open Names open Term +open EConstr open Libnames open Globnames open Genredexpr @@ -57,12 +58,12 @@ val wit_open_constr : val wit_constr_with_bindings : (constr_expr with_bindings, glob_constr_and_expr with_bindings, - EConstr.constr with_bindings delayed_open) genarg_type + constr with_bindings delayed_open) genarg_type val wit_bindings : (constr_expr bindings, glob_constr_and_expr bindings, - EConstr.constr bindings delayed_open) genarg_type + constr bindings delayed_open) genarg_type val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 20d9640fc..28ff6df83 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -27,7 +27,7 @@ TACTIC EXTEND reflexivity END TACTIC EXTEND exact - [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check (EConstr.of_constr c) ] + [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] END TACTIC EXTEND assumption @@ -39,35 +39,35 @@ TACTIC EXTEND etransitivity END TACTIC EXTEND cut - [ "cut" constr(c) ] -> [ Tactics.cut (EConstr.of_constr c) ] + [ "cut" constr(c) ] -> [ Tactics.cut c ] END TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check (EConstr.of_constr c) ] + [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] END TACTIC EXTEND vm_cast_no_check - [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check (EConstr.of_constr c) ] + [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ] END TACTIC EXTEND native_cast_no_check - [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check (EConstr.of_constr c) ] + [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ] END TACTIC EXTEND casetype - [ "casetype" constr(c) ] -> [ Tactics.case_type (EConstr.of_constr c) ] + [ "casetype" constr(c) ] -> [ Tactics.case_type c ] END TACTIC EXTEND elimtype - [ "elimtype" constr(c) ] -> [ Tactics.elim_type (EConstr.of_constr c) ] + [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ] END TACTIC EXTEND lapply - [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply (EConstr.of_constr c) ] + [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] END TACTIC EXTEND transitivity - [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some (EConstr.of_constr c)) ] + [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ] END (** Left *) @@ -297,7 +297,7 @@ END (* Generalize dependent *) TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep (EConstr.of_constr c) ] + [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] END (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index 99023fdbb..6b94da28a 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -77,15 +77,16 @@ let let_evar name typ = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma = ref sigma in - let _ = Typing.e_sort_of env sigma (EConstr.of_constr typ) in + let _ = Typing.e_sort_of env sigma typ in let sigma = Sigma.Unsafe.of_evar_map !sigma in let id = match name with | Names.Anonymous -> + let typ = EConstr.Unsafe.to_constr typ in let id = Namegen.id_of_name_using_hdchar env typ name in Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) | Names.Name id -> id in - let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) (EConstr.of_constr typ) in + let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in let tac = (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) in diff --git a/ltac/evar_tactics.mli b/ltac/evar_tactics.mli index e67540c05..41266e61c 100644 --- a/ltac/evar_tactics.mli +++ b/ltac/evar_tactics.mli @@ -16,4 +16,4 @@ val instantiate_tac : int -> Tacinterp.interp_sign * Glob_term.glob_constr -> val instantiate_tac_by_name : Id.t -> Tacinterp.interp_sign * Glob_term.glob_constr -> unit Proofview.tactic -val let_evar : Name.t -> Term.types -> unit Proofview.tactic +val let_evar : Name.t -> EConstr.types -> unit Proofview.tactic diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index b12187e18..7d4bccfad 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -38,12 +38,12 @@ val wit_lglob : val wit_lconstr : (constr_expr, Tacexpr.glob_constr_and_expr, - Constr.t) Genarg.genarg_type + EConstr.t) Genarg.genarg_type val wit_casted_constr : (constr_expr, Tacexpr.glob_constr_and_expr, - Constr.t) Genarg.genarg_type + EConstr.t) Genarg.genarg_type val glob : constr_expr Pcoq.Gram.entry val lglob : constr_expr Pcoq.Gram.entry diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index bf8481b52..65c75703b 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -47,16 +47,16 @@ let with_delayed_uconstr ist c tac = let replace_in_clause_maybe_by ist c1 c2 cl tac = with_delayed_uconstr ist c1 - (fun c1 -> replace_in_clause_maybe_by (EConstr.of_constr c1) c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac)) + (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac)) let replace_term ist dir_opt c cl = - with_delayed_uconstr ist c (fun c -> replace_term dir_opt (EConstr.of_constr c) cl) + with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) let clause = Pltac.clause_dft_concl TACTIC EXTEND replace ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by ist c1 (EConstr.of_constr c2) cl tac ] +-> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] END TACTIC EXTEND replace_term_left @@ -153,9 +153,9 @@ let injHyp id = injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } TACTIC EXTEND dependent_rewrite -| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b (EConstr.of_constr c) ] +| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] | [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ] - -> [ rewriteInHyp b (EConstr.of_constr c) id ] + -> [ rewriteInHyp b c id ] END (** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to @@ -163,20 +163,20 @@ END "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) TACTIC EXTEND cut_rewrite -| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b (EConstr.of_constr eqn) ] +| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ] | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] - -> [ cutRewriteInHyp b (EConstr.of_constr eqn) id ] + -> [ cutRewriteInHyp b eqn id ] END (**********************************************************************) (* Decompose *) TACTIC EXTEND decompose_sum -| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or (EConstr.of_constr c) ] +| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ] END TACTIC EXTEND decompose_record -| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and (EConstr.of_constr c) ] +| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ] END (**********************************************************************) @@ -185,7 +185,7 @@ END open Contradiction TACTIC EXTEND absurd - [ "absurd" constr(c) ] -> [ absurd (EConstr.of_constr c) ] + [ "absurd" constr(c) ] -> [ absurd c ] END let onSomeWithHoles tac = function @@ -235,7 +235,7 @@ END let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) = let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in with_delayed_uconstr ist c - (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (EConstr.of_constr c,NoBindings) true) + (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) TACTIC EXTEND rewrite_star | [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> @@ -362,7 +362,7 @@ let refine_tac ist simple c = let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> let Sigma (c, sigma, p) = c.delayed env sigma in - Sigma (EConstr.of_constr c, sigma, p) + Sigma (c, sigma, p) } in let refine = Refine.refine ~unsafe:true update in if simple then refine @@ -516,13 +516,13 @@ let add_transitivity_lemma left lem = (* Vernacular syntax *) TACTIC EXTEND stepl -| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true (EConstr.of_constr c) (Tacinterp.tactic_of_value ist tac) ] -| ["stepl" constr(c) ] -> [ step true (EConstr.of_constr c) (Proofview.tclUNIT ()) ] +| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ] +| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ] END TACTIC EXTEND stepr -| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false (EConstr.of_constr c) (Tacinterp.tactic_of_value ist tac) ] -| ["stepr" constr(c) ] -> [ step false (EConstr.of_constr c) (Proofview.tclUNIT ()) ] +| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ] +| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ] END VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF @@ -645,6 +645,8 @@ let subst_hole_with_term occ tc t = open Tacmach let hResolve id c occ t = + let c = EConstr.Unsafe.to_constr c in + let t = EConstr.Unsafe.to_constr t in Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let sigma = Sigma.to_evar_map sigma in @@ -819,8 +821,9 @@ END let eq_constr x y = Proofview.Goal.enter { enter = begin fun gl -> let evd = Tacmach.New.project gl in - if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () - else Tacticals.New.tclFAIL 0 (str "Not equal") + match EConstr.eq_constr_universes evd x y with + | Some _ -> Proofview.tclUNIT () + | None -> Tacticals.New.tclFAIL 0 (str "Not equal") end } TACTIC EXTEND constr_eq @@ -830,15 +833,13 @@ END TACTIC EXTEND constr_eq_nounivs | [ "constr_eq_nounivs" constr(x) constr(y) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - let x = EConstr.of_constr x in - let y = EConstr.of_constr y in if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ] END TACTIC EXTEND is_evar | [ "is_evar" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | Evar _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") ] @@ -871,14 +872,14 @@ has_evar c TACTIC EXTEND has_evar | [ "has_evar" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - if has_evar sigma (EConstr.of_constr x) then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") + if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") ] END TACTIC EXTEND is_hyp | [ "is_var" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | Var _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ] END @@ -886,7 +887,7 @@ END TACTIC EXTEND is_fix | [ "is_fix" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | Fix _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ] END;; @@ -894,7 +895,7 @@ END;; TACTIC EXTEND is_cofix | [ "is_cofix" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | CoFix _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ] END;; @@ -902,7 +903,7 @@ END;; TACTIC EXTEND is_ind | [ "is_ind" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | Ind _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ] END;; @@ -910,7 +911,7 @@ END;; TACTIC EXTEND is_constructor | [ "is_constructor" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | Construct _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ] END;; @@ -918,7 +919,7 @@ END;; TACTIC EXTEND is_proj | [ "is_proj" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | Proj _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ] END;; @@ -926,7 +927,7 @@ END;; TACTIC EXTEND is_const | [ "is_const" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma (EConstr.of_constr x) with + match EConstr.kind sigma x with | Const _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ] END;; @@ -1080,7 +1081,7 @@ let decompose l c = end } TACTIC EXTEND decompose -| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose (List.map EConstr.of_constr l) (EConstr.of_constr c) ] +| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] END (** library/keys *) diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index b5e56d93b..d4d3b9d66 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -28,7 +28,7 @@ TACTIC EXTEND eassumption END TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact (EConstr.of_constr c) ] +| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ] END let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases @@ -51,7 +51,7 @@ let eval_uconstrs ist cs = } in let map c = { delayed = fun env sigma -> let Sigma.Sigma (c, sigma, p) = c.delayed env sigma in - Sigma.Sigma (EConstr.of_constr c, sigma, p) + Sigma.Sigma (c, sigma, p) } in List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs @@ -151,7 +151,7 @@ TACTIC EXTEND autounfold_one TACTIC EXTEND autounfoldify | [ "autounfoldify" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - let db = match EConstr.kind sigma (EConstr.of_constr x) with + let db = match EConstr.kind sigma x with | Term.Const (c,_) -> Names.Label.to_string (Names.con_label c) | _ -> assert false in Eauto.autounfold ["core";db] Locusops.onConcl @@ -159,7 +159,7 @@ TACTIC EXTEND autounfoldify END TACTIC EXTEND unify -| ["unify" constr(x) constr(y) ] -> [ Tactics.unify (EConstr.of_constr x) (EConstr.of_constr y) ] +| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] | ["unify" constr(x) constr(y) "with" preident(base) ] -> [ let table = try Some (Hints.searchtable_map base) with Not_found -> None in match table with @@ -168,13 +168,13 @@ TACTIC EXTEND unify Tacticals.New.tclZEROMSG msg | Some t -> let state = Hints.Hint_db.transparent_state t in - Tactics.unify ~state (EConstr.of_constr x) (EConstr.of_constr y) + Tactics.unify ~state x y ] END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check (EConstr.of_constr x) Term.DEFAULTcast ] +| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ] END let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index a983a4fea..b7f0881f1 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -62,19 +62,19 @@ TACTIC EXTEND typeclasses_eauto END TACTIC EXTEND head_of_constr - [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h (EConstr.of_constr c) ] + [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ] END TACTIC EXTEND not_evar - [ "not_evar" constr(ty) ] -> [ not_evar (EConstr.of_constr ty) ] + [ "not_evar" constr(ty) ] -> [ not_evar ty ] END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground (EConstr.of_constr ty)) ] + [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ] END TACTIC EXTEND autoapply - [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply (EConstr.of_constr c) i) ] + [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ] END (** TODO: DEPRECATE *) diff --git a/ltac/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4 index 6a49ea830..905653281 100644 --- a/ltac/g_eqdecide.ml4 +++ b/ltac/g_eqdecide.ml4 @@ -23,5 +23,5 @@ TACTIC EXTEND decide_equality END TACTIC EXTEND compare -| [ "compare" constr(c1) constr(c2) ] -> [ compare (EConstr.of_constr c1) (EConstr.of_constr c2) ] +| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] END diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index bae5a516c..b1c4f58eb 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -265,7 +265,7 @@ TACTIC EXTEND setoid_reflexivity END TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some (EConstr.of_constr t)) ] + [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] END diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml index 934830f4d..b7dd37cdd 100644 --- a/ltac/pptactic.ml +++ b/ltac/pptactic.ml @@ -59,8 +59,8 @@ type 'a glob_extra_genarg_printer = 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> + (EConstr.constr -> std_ppcmds) -> + (EConstr.constr -> std_ppcmds) -> (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds @@ -1167,15 +1167,15 @@ module Make | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty - let pr_atomic_tactic_level env n t = + let pr_atomic_tactic_level env sigma n t = let prtac n (t:atomic_tactic_expr) = let pr = { pr_tactic = (fun _ _ -> str "<tactic>"); - pr_constr = (fun c -> pr_constr_env env Evd.empty (EConstr.Unsafe.to_constr c)); + pr_constr = (fun c -> pr_econstr_env env sigma c); pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); - pr_lconstr = (fun c -> pr_lconstr_env env Evd.empty (EConstr.Unsafe.to_constr c)); - pr_pattern = pr_constr_pattern_env env Evd.empty; - pr_lpattern = pr_lconstr_pattern_env env Evd.empty; + pr_lconstr = (fun c -> pr_leconstr_env env sigma c); + pr_pattern = pr_constr_pattern_env env sigma; + pr_lpattern = pr_lconstr_pattern_env env sigma; pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; @@ -1206,7 +1206,7 @@ module Make let pr_extend pr lev ml args = pr_extend_gen pr lev ml args - let pr_atomic_tactic env = pr_atomic_tactic_level env ltop + let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c end @@ -1255,7 +1255,7 @@ let declare_extra_genarg_pprule wit in let h x = let env = Global.env () in - h (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x + h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x in Genprint.register_print0 wit f g h @@ -1285,7 +1285,7 @@ let () = wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed c))))); + (Miscprint.pr_intro_pattern (fun c -> pr_econstr (fst (run_delayed c)))); Genprint.register_print0 wit_clause_dft_concl (pr_clauses (Some true) pr_lident) @@ -1296,7 +1296,7 @@ let () = wit_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_constr + Printer.pr_econstr ; Genprint.register_print0 wit_uconstr @@ -1308,25 +1308,25 @@ let () = wit_open_constr Ppconstr.pr_constr_expr (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_constr + Printer.pr_econstr ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) - (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern)); + (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; Genprint.register_print0 wit_bindings (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_bindings_no_with (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it))); + (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it))); + (fun it -> pr_with_bindings pr_econstr pr_leconstr (fst (run_delayed it))); Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_destruction_arg (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (run_delayed_destruction_arg it)); + (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it)); Genprint.register_print0 Stdarg.wit_int int int int; Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; diff --git a/ltac/pptactic.mli b/ltac/pptactic.mli index 86e3ea548..5fff3062d 100644 --- a/ltac/pptactic.mli +++ b/ltac/pptactic.mli @@ -34,8 +34,8 @@ type 'a glob_extra_genarg_printer = 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> + (EConstr.constr -> std_ppcmds) -> + (EConstr.constr -> std_ppcmds) -> (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds diff --git a/ltac/pptacticsig.mli b/ltac/pptacticsig.mli index 74ddd377a..dfbc3b3ed 100644 --- a/ltac/pptacticsig.mli +++ b/ltac/pptacticsig.mli @@ -61,7 +61,7 @@ module type Pp = sig val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds - val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds + val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> std_ppcmds val pr_hintbases : string list option -> std_ppcmds diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml index 288e12d0b..114b8dda0 100644 --- a/ltac/taccoerce.ml +++ b/ltac/taccoerce.ml @@ -9,6 +9,7 @@ open Util open Names open Term +open EConstr open Pattern open Misctypes open Genarg @@ -64,7 +65,7 @@ let to_constr v = Some c else if has_type v (topwit wit_constr_under_binders) then let vars, c = out_gen (topwit wit_constr_under_binders) v in - match vars with [] -> Some (EConstr.Unsafe.to_constr c) | _ -> None + match vars with [] -> Some c | _ -> None else None let of_uconstr c = in_gen (topwit wit_uconstr) c @@ -106,7 +107,7 @@ let coerce_to_constr_context v = else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) -let coerce_var_to_ident fresh env v = +let coerce_var_to_ident fresh env sigma v = let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then @@ -119,15 +120,16 @@ let coerce_var_to_ident fresh env v = | None -> fail () | Some c -> (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *) - if isVar c && not (fresh && is_variable env (destVar c)) then - destVar c + if isVar sigma c && not (fresh && is_variable env (destVar sigma c)) then + destVar sigma c else fail () (* Interprets, if possible, a constr to an identifier which may not be fresh but suitable to be given to the fresh tactic. Works for vars, constants, inductive, constructors and sorts. *) -let coerce_to_ident_not_fresh g env v = +let coerce_to_ident_not_fresh env sigma v = +let g = sigma in let id_of_name = function | Names.Anonymous -> Id.of_string "x" | Names.Name x -> x in @@ -143,7 +145,7 @@ let id_of_name = function match Value.to_constr v with | None -> fail () | Some c -> - match Constr.kind c with + match EConstr.kind sigma c with | Var id -> id | Meta m -> id_of_name (Evd.meta_name g m) | Evar (kn,_) -> @@ -169,7 +171,7 @@ let id_of_name = function | _ -> fail() -let coerce_to_intro_pattern env v = +let coerce_to_intro_pattern env sigma v = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then snd (out_gen (topwit wit_intro_pattern) v) @@ -177,14 +179,14 @@ let coerce_to_intro_pattern env v = let id = out_gen (topwit wit_var) v in IntroNaming (IntroIdentifier id) else match Value.to_constr v with - | Some c when isVar c -> + | Some c when isVar sigma c -> (* This happens e.g. in definitions like "Tac H = clear H; intro H" *) (* but also in "destruct H as (H,H')" *) - IntroNaming (IntroIdentifier (destVar c)) + IntroNaming (IntroIdentifier (destVar sigma c)) | _ -> raise (CannotCoerceTo "an introduction pattern") -let coerce_to_intro_pattern_naming env v = - match coerce_to_intro_pattern env v with +let coerce_to_intro_pattern_naming env sigma v = + match coerce_to_intro_pattern env sigma v with | IntroNaming pat -> pat | _ -> raise (CannotCoerceTo "a naming introduction pattern") @@ -212,7 +214,7 @@ let coerce_to_constr env v = | _ -> fail () else if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in - ([], EConstr.of_constr c) + ([], c) else if has_type v (topwit wit_constr_under_binders) then out_gen (topwit wit_constr_under_binders) v else if has_type v (topwit wit_var) then @@ -229,11 +231,10 @@ let coerce_to_uconstr env v = let coerce_to_closed_constr env v = let ids,c = coerce_to_constr env v in - let c = EConstr.Unsafe.to_constr c in let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in c -let coerce_to_evaluable_ref env v = +let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in let v = Value.normalize v in let ev = @@ -254,8 +255,8 @@ let coerce_to_evaluable_ref env v = | IndRef _ | ConstructRef _ -> fail () else match Value.to_constr v with - | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) - | Some c when isVar c -> EvalVarRef (destVar c) + | Some c when isConst sigma c -> EvalConstRef (Univ.out_punivs (destConst sigma c)) + | Some c when isVar sigma c -> EvalVarRef (destVar sigma c) | _ -> fail () in if Tacred.is_evaluable env ev then ev else fail () @@ -267,14 +268,14 @@ let coerce_to_constr_list env v = List.map map l | None -> raise (CannotCoerceTo "a term list") -let coerce_to_intro_pattern_list loc env v = +let coerce_to_intro_pattern_list loc env sigma v = match Value.to_list v with | None -> raise (CannotCoerceTo "an intro pattern list") | Some l -> - let map v = (loc, coerce_to_intro_pattern env v) in + let map v = (loc, coerce_to_intro_pattern env sigma v) in List.map map l -let coerce_to_hyp env v = +let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then @@ -285,31 +286,31 @@ let coerce_to_hyp env v = let id = out_gen (topwit wit_var) v in if is_variable env id then id else fail () else match Value.to_constr v with - | Some c when isVar c -> destVar c + | Some c when isVar sigma c -> destVar sigma c | _ -> fail () -let coerce_to_hyp_list env v = +let coerce_to_hyp_list env sigma v = let v = Value.to_list v in match v with | Some l -> - let map n = coerce_to_hyp env n in + let map n = coerce_to_hyp env sigma n in List.map map l | None -> raise (CannotCoerceTo "a variable list") (* Interprets a qualified name *) -let coerce_to_reference env v = +let coerce_to_reference env sigma v = let v = Value.normalize v in match Value.to_constr v with | Some c -> begin - try Globnames.global_of_constr c + try fst (Termops.global_of_constr sigma c) with Not_found -> raise (CannotCoerceTo "a reference") end | None -> raise (CannotCoerceTo "a reference") (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) -let coerce_to_quantified_hypothesis v = +let coerce_to_quantified_hypothesis sigma v = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in @@ -322,17 +323,17 @@ let coerce_to_quantified_hypothesis v = else if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with - | Some c when isVar c -> NamedHyp (destVar c) + | Some c when isVar sigma c -> NamedHyp (destVar sigma c) | _ -> raise (CannotCoerceTo "a quantified hypothesis") (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) -let coerce_to_decl_or_quant_hyp env v = +let coerce_to_decl_or_quant_hyp env sigma v = let v = Value.normalize v in if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else - try coerce_to_quantified_hypothesis v + try coerce_to_quantified_hypothesis sigma v with CannotCoerceTo _ -> raise (CannotCoerceTo "a declared or quantified hypothesis") diff --git a/ltac/taccoerce.mli b/ltac/taccoerce.mli index 3049aff7e..9c4ac5265 100644 --- a/ltac/taccoerce.mli +++ b/ltac/taccoerce.mli @@ -9,6 +9,7 @@ open Util open Names open Term +open EConstr open Misctypes open Pattern open Genarg @@ -48,16 +49,16 @@ end (** {5 Coercion functions} *) -val coerce_to_constr_context : Value.t -> EConstr.constr +val coerce_to_constr_context : Value.t -> constr -val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t +val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t -val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t +val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t -val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr +val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : - Environ.env -> Value.t -> intro_pattern_naming_expr + Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr val coerce_to_hint_base : Value.t -> string @@ -70,22 +71,22 @@ val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr val coerce_to_evaluable_ref : - Environ.env -> Value.t -> evaluable_global_reference + Environ.env -> Evd.evar_map -> Value.t -> evaluable_global_reference val coerce_to_constr_list : Environ.env -> Value.t -> constr list val coerce_to_intro_pattern_list : - Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns + Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns -val coerce_to_hyp : Environ.env -> Value.t -> Id.t +val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t -val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list +val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list -val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference +val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> Globnames.global_reference -val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis +val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis -val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis +val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis val coerce_to_int_or_var_list : Value.t -> int or_var list diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index b4d2b1e50..1fe6dbdd0 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -239,12 +239,12 @@ let pr_value env v = else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in match env with - | Some (env,sigma) -> pr_lconstr_env env sigma (EConstr.Unsafe.to_constr c) + | Some (env,sigma) -> pr_leconstr_env env sigma c | _ -> str "a term" else if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in match env with - | Some (env,sigma) -> pr_lconstr_env env sigma c + | Some (env,sigma) -> pr_leconstr_env env sigma c | _ -> str "a term" else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in @@ -282,7 +282,7 @@ let pr_inspect env expr result = (* Transforms an id into a constr if possible, or fails with Not_found *) let constr_of_id env id = - Term.mkVar (let _ = Environ.lookup_named id env in id) + EConstr.mkVar (let _ = Environ.lookup_named id env in id) (** Generic arguments : table of interpretation functions *) @@ -334,7 +334,7 @@ let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 let extend_values_with_bindings (ln,lm) lfun = let of_cub c = match c with - | [], c -> Value.of_constr (EConstr.Unsafe.to_constr c) + | [], c -> Value.of_constr c | _ -> in_gen (topwit wit_constr_under_binders) c in (* For compatibility, bound variables are visible only if no other @@ -385,7 +385,7 @@ let interp_ltac_var coerce ist env locid = with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") let interp_ident ist env sigma id = - try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id) + try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (dloc,id) with Not_found -> id (* Interprets an optional identifier, bound or fresh *) @@ -394,11 +394,11 @@ let interp_name ist env sigma = function | Name id -> Name (interp_ident ist env sigma id) let interp_intro_pattern_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id) with Not_found -> IntroNaming (IntroIdentifier id) let interp_intro_pattern_naming_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id) with Not_found -> IntroIdentifier id let interp_int ist locid = @@ -423,14 +423,14 @@ let interp_int_or_var_list ist l = (* Interprets a bound variable (especially an existing hypothesis) *) let interp_hyp ist env sigma (loc,id as locid) = (* Look first in lfun for a value coercible to a variable *) - try try_interp_ltac_var (coerce_to_hyp env) ist (Some (env,sigma)) locid + try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = - try coerce_to_hyp_list env (Id.Map.find id ist.lfun) + try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x] let interp_hyp_list ist env sigma l = @@ -445,7 +445,7 @@ let interp_move_location ist env sigma = function let interp_reference ist env sigma = function | ArgArg (_,r) -> r | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_reference env) ist (Some (env,sigma)) (loc, id) + try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id) with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) @@ -469,7 +469,7 @@ let interp_evaluable ist env sigma = function end | ArgArg (r,None) -> r | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id) + try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id) with Not_found -> try try_interp_evaluable env (loc, id) with Not_found -> error_global_not_found ~loc (qualid_of_ident id) @@ -540,7 +540,7 @@ let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = let extract_ident ist env sigma id = - try try_interp_ltac_var (coerce_to_ident_not_fresh sigma env) + try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma) ist (Some (env,sigma)) (dloc,id) with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in @@ -561,24 +561,24 @@ let interp_fresh_id ist env sigma l = Tactics.fresh_id_in_env avoid id env (* Extract the uconstr list from lfun *) -let extract_ltac_constr_context ist env = +let extract_ltac_constr_context ist env sigma = let open Glob_term in - let add_uconstr id env v map = + let add_uconstr id v map = try Id.Map.add id (coerce_to_uconstr env v) map with CannotCoerceTo _ -> map in - let add_constr id env v map = + let add_constr id v map = try Id.Map.add id (coerce_to_constr env v) map with CannotCoerceTo _ -> map in - let add_ident id env v map = - try Id.Map.add id (coerce_var_to_ident false env v) map + let add_ident id v map = + try Id.Map.add id (coerce_var_to_ident false env sigma v) map with CannotCoerceTo _ -> map in let fold id v {idents;typed;untyped} = - let idents = add_ident id env v idents in - let typed = add_constr id env v typed in - let untyped = add_uconstr id env v untyped in + let idents = add_ident id v idents in + let typed = add_constr id v typed in + let untyped = add_uconstr id v untyped in { idents ; typed ; untyped } in let empty = { idents = Id.Map.empty ;typed = Id.Map.empty ; untyped = Id.Map.empty } in @@ -586,11 +586,11 @@ let extract_ltac_constr_context ist env = (** Significantly simpler than [interp_constr], to interpret an untyped constr, it suffices to adjoin a closure environment. *) -let interp_uconstr ist env = function +let interp_uconstr ist env sigma = function | (term,None) -> - { closure = extract_ltac_constr_context ist env ; term } + { closure = extract_ltac_constr_context ist env sigma; term } | (_,Some ce) -> - let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env in + let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env sigma in let ltacvars = { Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); ltac_bound = Id.Map.domain ist.lfun; @@ -598,7 +598,7 @@ let interp_uconstr ist env = function { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } let interp_gen kind ist allow_patvar flags env sigma (c,ce) = - let constrvars = extract_ltac_constr_context ist env in + let constrvars = extract_ltac_constr_context ist env sigma in let vars = { Pretyping.ltac_constrs = constrvars.typed; Pretyping.ltac_uconstrs = constrvars.untyped; @@ -636,10 +636,11 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) c in + let c = EConstr.of_constr c in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) - Proofview.NonLogical.run (db_constr (curr_debug ist) env c); + Proofview.NonLogical.run (db_constr (curr_debug ist) env evd c); (evd,c) let constr_flags = { @@ -691,7 +692,7 @@ let interp_pure_open_constr ist = let interp_typed_pattern ist env sigma (_,c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in - pattern_of_constr env sigma (EConstr.of_constr c) + pattern_of_constr env sigma c (* Interprets a constr expression *) let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = @@ -733,10 +734,10 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = prioritary to an evaluable reference and otherwise to a constr (it is an encoding to satisfy the "union" type given to Simpl) *) let coerce_eval_ref_or_constr x = - try Inl (coerce_to_evaluable_ref env x) + try Inl (coerce_to_evaluable_ref env sigma x) with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in - Inr (pattern_of_constr env sigma (EConstr.of_constr c)) in + Inr (pattern_of_constr env sigma c) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) with Not_found -> error_global_not_found ~loc (qualid_of_ident id)) @@ -746,12 +747,11 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let interp_constr_with_occurrences_and_name_as_list = interp_constr_in_compound_list - (fun c -> ((AllOccurrences,EConstr.of_constr c),Anonymous)) + (fun c -> ((AllOccurrences,c),Anonymous)) (function ((occs,c),Anonymous) when occs == AllOccurrences -> c | _ -> raise Not_found) (fun ist env sigma (occ_c,na) -> let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in - let c_interp = (fst c_interp, EConstr.of_constr (snd c_interp)) in sigma, (c_interp, interp_name ist env sigma na)) @@ -784,8 +784,7 @@ let interp_may_eval f ist env sigma = function let (sigma,c_interp) = f ist env sigma c in let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma (EConstr.of_constr c_interp) in - let c = EConstr.Unsafe.to_constr c in + let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma c_interp in (Sigma.to_evar_map sigma, c) | ConstrContext ((loc,s),c) -> (try @@ -793,8 +792,10 @@ let interp_may_eval f ist env sigma = function let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let ctxt = EConstr.Unsafe.to_constr ctxt in let evdref = ref sigma in + let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in + let c = EConstr.of_constr c in !evdref , c with | Not_found -> @@ -802,8 +803,8 @@ let interp_may_eval f ist env sigma = function (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - let (sigma, t) = Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) in - (sigma, EConstr.Unsafe.to_constr t) + let (sigma, t) = Typing.type_of ~refresh:true env sigma c_interp in + (sigma, t) | ConstrTerm c -> try f ist env sigma c @@ -833,7 +834,7 @@ let interp_constr_may_eval ist env sigma c = (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) - Proofview.NonLogical.run (db_constr (curr_debug ist) env csr); + Proofview.NonLogical.run (db_constr (curr_debug ist) env sigma csr); sigma , csr end @@ -845,7 +846,7 @@ let rec message_of_value v = Ftactic.return (str "<tactic>") else if has_type v (topwit wit_constr) then let v = out_gen (topwit wit_constr) v in - Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) v) end } + Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end } else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in Ftactic.nf_enter { enter = begin fun gl -> @@ -922,7 +923,6 @@ and interp_intro_pattern_action ist env sigma = function let c = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr ist env sigma c in - let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) } in let sigma,ipat = interp_intro_pattern ist env sigma ipat in @@ -939,7 +939,7 @@ and interp_or_and_intro_pattern ist env sigma = function and interp_intro_pattern_list_as_list ist env sigma = function | [loc,IntroNaming (IntroIdentifier id)] as l -> - (try sigma, coerce_to_intro_pattern_list loc env (Id.Map.find id ist.lfun) + (try sigma, coerce_to_intro_pattern_list loc env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> List.fold_map (interp_intro_pattern ist env) sigma l) | l -> List.fold_map (interp_intro_pattern ist env) sigma l @@ -951,7 +951,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None | Some (ArgVar (loc,id)) -> - (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with + (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern")) @@ -969,31 +969,25 @@ let interp_in_hyp_as ist env sigma (id,ipat) = let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in sigma,(interp_hyp ist env sigma id,ipat) -let interp_quantified_hypothesis ist = function - | AnonHyp n -> AnonHyp n - | NamedHyp id -> - try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) - with Not_found -> NamedHyp id - -let interp_binding_name ist = function +let interp_binding_name ist sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(dloc,id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env) ist (Some (env,sigma)) (dloc,id) + (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,id) with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,b,c) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,interp_binding_name ist b,c) + sigma, (loc,interp_binding_name ist sigma b,c) let interp_bindings ist env sigma = function | NoBindings -> @@ -1008,14 +1002,11 @@ let interp_bindings ist env sigma = function let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in let sigma, c = interp_open_constr ist env sigma c in - let c = EConstr.of_constr c in - let bl = Miscops.map_bindings EConstr.of_constr bl in sigma, (c,bl) let interp_open_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in let sigma, c = interp_open_constr ist env sigma c in - let (c, bl) = Miscops.map_with_bindings EConstr.of_constr (c, bl) in sigma, (c, bl) let loc_of_bindings = function @@ -1053,7 +1044,7 @@ let interp_destruction_arg ist gl arg = then keep,ElimOnIdent (loc,id') else (keep, ElimOnConstr { delayed = begin fun env sigma -> - try Sigma.here (EConstr.of_constr (constr_of_id env id'), NoBindings) sigma + try Sigma.here (constr_of_id env id', NoBindings) sigma with Not_found -> user_err ~loc ~hdr:"interp_destruction_arg" ( pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") @@ -1075,7 +1066,7 @@ let interp_destruction_arg ist gl arg = keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) } + | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) } with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then @@ -1085,7 +1076,6 @@ let interp_destruction_arg ist gl arg = let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in - let c = EConstr.of_constr c in Sigma.Unsafe.of_pair ((c,NoBindings), sigma) } in keep,ElimOnConstr f @@ -1365,7 +1355,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t = Ftactic.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let c = interp_uconstr ist env c in + let c = interp_uconstr ist env (Sigma.to_evar_map sigma) c in let Sigma (c, sigma, p) = (type_uconstr ist c).delayed env sigma in Sigma (Ftactic.return (Value.of_constr c), sigma, p) end } @@ -1468,7 +1458,7 @@ and interp_letin ist llc u = and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = let (>>=) = Ftactic.bind in let lctxt = Id.Map.map interp_context context in - let hyp_subst = Id.Map.map (EConstr.Unsafe.to_constr %> Value.of_constr) terms in + let hyp_subst = Id.Map.map Value.of_constr terms in let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in let ist = { ist with lfun } in val_interp ist lhs >>= fun v -> @@ -1522,7 +1512,6 @@ and interp_match ist lz constr lmr = Proofview.tclZERO ~info e end end >>= fun constr -> - let constr = EConstr.of_constr constr in Ftactic.enter { enter = begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in @@ -1597,7 +1586,7 @@ and interp_genarg_var_list ist x = end } (* Interprets tactic expressions : returns a "constr" *) -and interp_ltac_constr ist e : constr Ftactic.t = +and interp_ltac_constr ist e : EConstr.t Ftactic.t = let (>>=) = Ftactic.bind in begin Proofview.tclORELSE (val_interp ist e) @@ -1625,7 +1614,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = debugging_step ist (fun () -> Pptactic.pr_glob_tactic env e ++ fnl() ++ str " has value " ++ fnl() ++ - pr_constr_env env sigma cresult) + pr_econstr_env env sigma cresult) end <*> Ftactic.return cresult with CannotCoerceTo _ -> @@ -1645,7 +1634,8 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic = | Some e -> Proofview.tclUNIT e | None -> Proofview.tclENV end >>= fun env -> - let name () = Pptactic.pr_atomic_tactic env tacexpr in + Proofview.tclEVARMAP >>= fun sigma -> + let name () = Pptactic.pr_atomic_tactic env sigma tacexpr in Proofview.Trace.name_tactic name tac (* Interprets a primitive tactic *) @@ -1712,7 +1702,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = interp_type ist env sigma c in - sigma , (interp_ident ist env sigma id,n,EConstr.of_constr c_interp) in + sigma , (interp_ident ist env sigma id,n,c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in @@ -1727,7 +1717,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = interp_type ist env sigma c in - sigma , (interp_ident ist env sigma id,EConstr.of_constr c_interp) in + sigma , (interp_ident ist env sigma id,c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in @@ -1742,7 +1732,6 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in - let c = EConstr.of_constr c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (Option.map (interp_tactic ist)) t in Tacticals.New.tclWITHHOLES false @@ -1770,7 +1759,6 @@ and interp_atomic ist tac : unit Proofview.tactic = if Locusops.is_nowhere clp then (* We try to fully-typecheck the term *) let (sigma,c_interp) = interp_constr ist env sigma c in - let c_interp = EConstr.of_constr c_interp in let let_tac b na c cl eqpat = let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in @@ -1789,7 +1777,6 @@ and interp_atomic ist tac : unit Proofview.tactic = Tactics.letin_pat_tac with_eq na c cl in let (sigma',c) = interp_pure_open_constr ist env sigma c in - let c = EConstr.of_constr c in name_atomic ~env (TacLetTac(na,c,clp,b,eqpat)) (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) @@ -1849,7 +1836,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let sigma = Sigma.to_evar_map sigma in @@ -1859,7 +1846,6 @@ and interp_atomic ist tac : unit Proofview.tactic = then interp_type ist (pf_env gl) sigma c else interp_constr ist (pf_env gl) sigma c in - let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) end } in Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) @@ -1876,14 +1862,13 @@ and interp_atomic ist tac : unit Proofview.tactic = let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in try let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_constr ist env sigma c in - let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) with e when to_catch e (* Hack *) -> user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") @@ -1922,7 +1907,6 @@ and interp_atomic ist tac : unit Proofview.tactic = | None -> sigma , None | Some c -> let (sigma,c_interp) = interp_constr ist env sigma c in - let c_interp = EConstr.of_constr c_interp in sigma , Some c_interp in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in @@ -1949,7 +1933,6 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let (sigma,c_interp) = interp_constr ist env sigma c in - let c_interp = EConstr.of_constr c_interp in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let hyps = interp_hyp_list ist env sigma idl in let tac = name_atomic ~env @@ -2059,7 +2042,6 @@ end } let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma -> let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in - let bl = Miscops.map_bindings EConstr.of_constr bl in Sigma.Unsafe.of_pair (bl, sigma) } @@ -2099,7 +2081,7 @@ let () = let () = register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl -> - Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c) + Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c) end }) (***************************************************************************) diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 2b0324e24..c657a11f1 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -9,6 +9,7 @@ open Names open Tactic_debug open Term +open EConstr open Tacexpr open Genarg open Redexpr diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index be1123d5c..b2601ad32 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -51,8 +51,7 @@ let db_pr_goal gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let penv = print_named_context env in - let concl = EConstr.Unsafe.to_constr concl in - let pc = print_constr_env env concl in + let pc = print_constr_env env (Tacmach.New.project gl) concl in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () @@ -224,11 +223,11 @@ let is_debug db = return (Int.equal skip 0) (* Prints a constr *) -let db_constr debug env c = +let db_constr debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c) + msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c) else return () (* Prints the pattern rule *) @@ -248,20 +247,20 @@ let hyp_bound = function | Name id -> str " (bound to " ++ pr_id id ++ str ")" (* Prints a matched hypothesis *) -let db_matched_hyp debug env (id,_,c) ido = +let db_matched_hyp debug env sigma (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ - str " has been matched: " ++ print_constr_env env c) + str " has been matched: " ++ print_constr_env env sigma c) else return () (* Prints the matched conclusion *) -let db_matched_concl debug env c = +let db_matched_concl debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c) + msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c) else return () (* Prints a success message when the goal has been matched *) diff --git a/ltac/tactic_debug.mli b/ltac/tactic_debug.mli index 520fb41ef..7745d9b7b 100644 --- a/ltac/tactic_debug.mli +++ b/ltac/tactic_debug.mli @@ -11,6 +11,7 @@ open Pattern open Names open Tacexpr open Term +open EConstr open Evd (** TODO: Move those definitions somewhere sensible *) @@ -34,7 +35,7 @@ val debug_prompt : val db_initialize : unit Proofview.NonLogical.t (** Prints a constr *) -val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t +val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t (** Prints the pattern rule *) val db_pattern_rule : @@ -42,10 +43,10 @@ val db_pattern_rule : (** Prints a matched hypothesis *) val db_matched_hyp : - debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t + debug_info -> env -> evar_map -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t (** Prints the matched conclusion *) -val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t +val db_matched_concl : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t (** Prints a success message when the goal has been matched *) val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t diff --git a/ltac/tauto.ml b/ltac/tauto.ml index a4faf438a..707154a30 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -25,7 +25,7 @@ let () = Mltop.add_known_module tauto_plugin let assoc_var s ist = let v = Id.Map.find (Names.Id.of_string s) ist.lfun in match Value.to_constr v with - | Some c -> EConstr.of_constr c + | Some c -> c | None -> failwith "tauto: anomaly" (** Parametrization of tauto *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 102efe55b..0a980c03b 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -497,10 +497,10 @@ let rec inst_pattern subst = function args t let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (constr_of_term (term uf i)) ++ str "]" + Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" let pr_term t = str "[" ++ - Termops.print_constr (constr_of_term t) ++ str "]" + Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -615,7 +615,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr prf ++ str " : " ++ + (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); add_equality state prf s t end @@ -623,7 +623,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr prf ++ str " : " ++ + (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index a4ed4798a..62892973d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -414,6 +414,7 @@ let build_term_to_complete uf meta pac = let cc_tactic depth additionnal_terms = Proofview.Goal.nf_enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (fun () -> Pp.str "Reading subgoal ...") in let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in @@ -448,7 +449,7 @@ let cc_tactic depth additionnal_terms = str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - (EConstr.Unsafe.to_constr %> Termops.print_constr_env env) + (Termops.print_constr_env env sigma) terms_to_complete ++ str ")\"," end ++ diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index b787e824f..6f6811334 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -18,9 +18,9 @@ DECLARE PLUGIN "cc_plugin" TACTIC EXTEND cc [ "congruence" ] -> [ congruence_tac 1000 [] ] |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 (List.map EConstr.of_constr l) ] + |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> - [ congruence_tac n (List.map EConstr.of_constr l) ] + [ congruence_tac n l ] END TACTIC EXTEND f_equal diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 59a0bb5a2..93b98263e 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -206,6 +206,8 @@ let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) = instr let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) = + let pconstr1 c = pconstr1 (EConstr.of_constr c) in + let pconstr2 c = pconstr2 (EConstr.of_constr c) in pr_gen_proof_instr (fun st -> pr_statement pconstr1 st) pconstr2 diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a6f971703..560242bf2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -58,7 +58,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = | None -> mt () | Some b -> let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in - spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed (EConstr.Unsafe.to_constr %> prc) (EConstr.Unsafe.to_constr %> prlc) b) + spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) ARGUMENT EXTEND fun_ind_using @@ -108,8 +108,9 @@ TACTIC EXTEND newfunind let c = match cl with | [] -> assert false | [c] -> c - | c::cl -> applist(c,cl) + | c::cl -> EConstr.applist(c,cl) in + let c = EConstr.Unsafe.to_constr c in Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] END (***** debug only ***) @@ -119,8 +120,9 @@ TACTIC EXTEND snewfunind let c = match cl with | [] -> assert false | [c] -> c - | c::cl -> applist(c,cl) + | c::cl -> EConstr.applist(c,cl) in + let c = EConstr.Unsafe.to_constr c in Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] END diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 5f906a8da..a6749c347 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin" DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute lt ] +| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ] END diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 79c429615..40c1028e5 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -23,7 +23,6 @@ let cont = Id.of_string "cont" let x = Id.of_string "x" let make_cont (k : Val.t) (c : EConstr.t) = - let c = EConstr.Unsafe.to_constr c in let c = Tacinterp.Value.of_constr c in let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in @@ -33,8 +32,8 @@ TACTIC EXTEND quote [ "quote" ident(f) ] -> [ quote f [] ] | [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] | [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) (EConstr.of_constr c) f [] ] + [ gen_quote (make_cont k) c f [] ] | [ "quote" ident(f) "[" ne_ident_list(lc) "]" "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) (EConstr.of_constr c) f lc ] + [ gen_quote (make_cont k) c f lc ] END diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 13cf8330b..b1882ae8a 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -30,7 +30,7 @@ END TACTIC EXTEND closed_term [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ closed_term (EConstr.of_constr t) l ] + [ closed_term t l ] END open Pptactic @@ -90,11 +90,7 @@ END TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ - let lH = List.map EConstr.of_constr lH in - let lrt = List.map EConstr.of_constr lrt in - let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t - ] + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ] END let pr_field_mod = function @@ -129,9 +125,5 @@ END TACTIC EXTEND field_lookup | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ - let lH = List.map EConstr.of_constr lH in - let lt = List.map EConstr.of_constr lt in - let (t,l) = List.sep_last lt in field_lookup f lH l t - ] + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index c0eeff8d7..ce2c558ae 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -183,7 +183,7 @@ let dummy_goal env sigma = {Evd.it = gl; Evd.sigma = sigma} let constr_of v = match Value.to_constr v with - | Some c -> c + | Some c -> EConstr.Unsafe.to_constr c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -203,7 +203,6 @@ let get_res = let exec_tactic env evd n f args = let fold arg (i, vars, lfun) = - let arg = EConstr.Unsafe.to_constr arg in let id = Id.of_string ("x" ^ string_of_int i) in let x = Reference (ArgVar (Loc.ghost, id)) in (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun) @@ -730,7 +729,7 @@ let make_term_list env evd carrier rl = (plapp evd coq_nil [|carrier|]) in Typing.e_solve_evars env evd l -let carg = Tacinterp.Value.of_constr +let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c) let tacarg expr = Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 9798fa11c..9dcc6c4cc 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1030,7 +1030,7 @@ let interp_constr = interp_wit wit_constr let interp_open_constr ist gl gc = interp_wit wit_open_constr ist gl gc let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c -let interp_term ist gl (_, c) = (interp_open_constr ist gl c) +let interp_term ist gl (_, c) = on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c) let pr_ssrterm _ _ _ = pr_term let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with | Tok.KEYWORD "(" -> '(' diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index d4b46c046..875e4a118 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -208,6 +208,6 @@ let split_tycon loc env evd tycon = let valcon_of_tycon x = x let lift_tycon n = Option.map (lift n) -let pr_tycon env = function +let pr_tycon env sigma = function None -> str "None" - | Some t -> Termops.print_constr_env env (EConstr.Unsafe.to_constr t) + | Some t -> Termops.print_constr_env env sigma t diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 9c03a6e3f..2f7ac4efb 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -43,5 +43,5 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts (** {6 debug pretty-printer:} *) -val pr_tycon : env -> type_constraint -> Pp.std_ppcmds +val pr_tycon : env -> evar_map -> type_constraint -> Pp.std_ppcmds diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a0d8faab4..09b99983c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -429,7 +429,7 @@ let protected_get_type_of env sigma c = try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> user_err - (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++ + (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") let pretype_id pretype k0 loc env evdref lvar id = @@ -1225,6 +1225,7 @@ let type_uconstr ?(flags = constr_flags) } in let sigma = Sigma.to_evar_map sigma in let (sigma, c) = understand_ltac flags env sigma vars expected_type term in + let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) end } diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2f3ce3afa..a1602088a 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -119,7 +119,7 @@ val understand_judgment_tcc : env -> evar_map ref -> val type_uconstr : ?flags:inference_flags -> ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open + Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 8362a2a26..bc9e3a1f4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -191,7 +191,7 @@ let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (t,con_pp,proji_sp_pp) -> strbrk "Projection value has no head constant: " - ++ Termops.print_constr t ++ strbrk " in canonical instance " + ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) @@ -256,8 +256,8 @@ let add_canonical_structure warn o = in match ocs with | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table; | Some (c, cs) -> - let old_can_s = (Termops.print_constr cs.o_DEF) - and new_can_s = (Termops.print_constr s.o_DEF) in + let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF)) + and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 90c5b241b..bc5c629f4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -210,7 +210,7 @@ module Cst_stack = struct let pr l = let open Pp in - let p_c c = Termops.print_constr (EConstr.Unsafe.to_constr c) in + let p_c c = Termops.print_constr c in prlist_with_sep pr_semicolon (fun (c,params,args) -> hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++ @@ -606,7 +606,7 @@ type local_state_reduction_function = evar_map -> state -> state let pr_state (tm,sk) = let open Pp in - let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in + let pr c = Termops.print_constr c in h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) let local_assum (na, t) = @@ -835,7 +835,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let rec whrec cst_l (x, stack) = let () = if !debug_RAKAM then let open Pp in - let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in + let pr c = Termops.print_constr c in Feedback.msg_notice (h 0 (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 233b58e91..c6fad1a34 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -671,16 +671,13 @@ let eta_constructor_app env sigma f l1 term = | _ -> assert false) | _ -> assert false -let print_constr_env env c = - print_constr_env env (EConstr.Unsafe.to_constr c) - let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn = let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in let () = if !debug_unification then - Feedback.msg_debug (print_constr_env curenv cM ++ str" ~= " ++ print_constr_env curenv cN) + Feedback.msg_debug (print_constr_env curenv sigma cM ++ str" ~= " ++ print_constr_env curenv sigma cN) in match (EConstr.kind sigma cM, EConstr.kind sigma cN) with | Meta k1, Meta k2 -> diff --git a/printing/printer.ml b/printing/printer.ml index 2a30681bf..4a6c83bd7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -60,7 +60,10 @@ let pr_constr_goal_style_env env = pr_constr_core true env let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c - (* NB do not remove the eta-redexes! Global.env() has side-effects... *) +let pr_leconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.to_constr sigma c) +let pr_econstr_env env sigma c = pr_constr_env env sigma (EConstr.to_constr sigma c) + +(* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = let (sigma, env) = get_current_context () in pr_lconstr_env env sigma t @@ -71,15 +74,18 @@ let pr_constr t = let pr_open_lconstr (_,c) = pr_lconstr c let pr_open_constr (_,c) = pr_constr c +let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c) +let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c) + let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) (* we also need to preserve the actual names of the patterns *) (* So what to do? *) let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in - pr (Termops.push_rels_assum assums env) sigma (EConstr.Unsafe.to_constr c) + pr (Termops.push_rels_assum assums env) sigma c -let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env -let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env +let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env +let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env let pr_constr_under_binders c = let (sigma, env) = get_current_context () in @@ -147,7 +153,7 @@ let pr_constr_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr - (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) + (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma (EConstr.Unsafe.to_constr t))) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" diff --git a/printing/printer.mli b/printing/printer.mli index 20032012a..7521468e2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -38,6 +38,10 @@ val safe_pr_lconstr : constr -> std_ppcmds val safe_pr_constr_env : env -> evar_map -> constr -> std_ppcmds val safe_pr_constr : constr -> std_ppcmds +val pr_econstr_env : env -> evar_map -> EConstr.t -> std_ppcmds +val pr_econstr : EConstr.t -> std_ppcmds +val pr_leconstr_env : env -> evar_map -> EConstr.t -> std_ppcmds +val pr_leconstr : EConstr.t -> std_ppcmds val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds val pr_open_constr : open_constr -> std_ppcmds diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 393e958d3..7269c61e3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -575,10 +575,9 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma (* Pretty-print *) let pr_clenv clenv = - let inj = EConstr.Unsafe.to_constr in h 0 - (str"TEMPL: " ++ print_constr (inj clenv.templval.rebus) ++ - str" : " ++ print_constr (inj clenv.templtyp.rebus) ++ fnl () ++ + (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ + str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ pr_evar_map (Some 2) clenv.evd) (****************************************************************) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 8878051c8..0fe5c73f1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -11,6 +11,7 @@ open CErrors open Util open Names open Term +open EConstr open Declarations open Globnames open Genredexpr @@ -200,9 +201,6 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) -let out_with_occurrences' (occs,c) = - (Locusops.occurrences_map (List.map out_arg) occs, EConstr.of_constr c) - let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl @@ -242,8 +240,8 @@ let reduction_of_red_expr env = (e_red (strong_cbn (make_flag f)), DEFAULTcast) | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) - | Fold cl -> (e_red (fold_commands (List.map EConstr.of_constr cl)),DEFAULTcast) - | Pattern lp -> (pattern_occs (List.map out_with_occurrences' lp),DEFAULTcast) + | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) + | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> @@ -256,9 +254,12 @@ let reduction_of_red_expr env = in reduction_of_red_expr +let subst_mps subst c = + EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) + let subst_red_expr subs = Miscops.map_red_expr_gen - (Mod_subst.subst_mps subs) + (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) (Patternops.subst_pattern subs) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index d4c2c4a6c..45e461066 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -10,6 +10,7 @@ open Names open Term +open EConstr open Pattern open Genredexpr open Reductionops diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7ffb30fa8..3641ad74d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -144,7 +144,7 @@ open Pp let db_pr_goal sigma g = let env = Goal.V82.env sigma g in let penv = print_named_context env in - let pc = print_constr_env env (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in + let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () diff --git a/tactics/auto.ml b/tactics/auto.ml index 4218be0bb..b548f8b92 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -152,7 +152,7 @@ let conclPattern concl pat tac = let open Genarg in let open Geninterp in let inj c = match val_tag (topwit Stdarg.wit_constr) with - | Val.Base tag -> Val.Dyn (tag, EConstr.Unsafe.to_constr c) + | Val.Base tag -> Val.Dyn (tag, c) | _ -> assert false in let fold id c accu = Id.Map.add id (inj c) accu in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 574f1c6f3..4e833eb55 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -51,7 +51,7 @@ open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let inj_with_occurrences e = (AllOccurrences,EConstr.Unsafe.to_constr e) +let inj_with_occurrences e = (AllOccurrences,e) let dloc = Loc.ghost @@ -922,7 +922,7 @@ let reduction_clause redexp cl = let reduce redexp cl = let trace () = let open Printer in - let pr = (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern) in + let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in Pp.(hov 2 (Pputils.pr_red_expr pr str redexp)) in Proofview.Trace.name_tactic trace begin |