diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 18:18:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 (patch) | |
| tree | ae729d05933776d718905029f0a87722716ec57f /plugins/cc | |
| parent | 531590c223af42c07a93142ab0cea470a98964e6 (diff) | |
Ltac now uses evar-based constrs.
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 8 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 3 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 4 |
3 files changed, 8 insertions, 7 deletions
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 |