diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.mlg | 14 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 |
2 files changed, 1 insertions, 15 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 2bc79d45d4..8946587a02 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -47,20 +47,6 @@ let ()= declare_int_option gdopt -let ()= - let congruence_depth=ref 100 in - let gdopt= - { optdepr=true; (* noop *) - optname="Congruence Depth"; - optkey=["Congruence";"Depth"]; - optread=(fun ()->Some !congruence_depth); - optwrite= - (function - None->congruence_depth:=0 - | Some i->congruence_depth:=(max i 0))} - in - declare_int_option gdopt - let default_intuition_tac = let tac _ _ = Auto.h_auto None [] None in let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 9ff05c33e4..7d84ee6851 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -231,7 +231,7 @@ let print_cmap map= let print_entry c l s= let env = Global.env () in let sigma = Evd.from_env env in - let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in + let xc=Constrextern.extern_constr env sigma (EConstr.of_constr c) in str "| " ++ prlist Printer.pr_global l ++ str " : " ++ |