diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 12:19:35 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 12:19:35 +0000 |
| commit | f0e24c6a8b66e86a22370fcc45d1f3e7543496fd (patch) | |
| tree | a31bdda34c4380c864e494f82b2a5e0dbb122a98 /contrib/first-order | |
| parent | 450763ee0152a75881a8618172cc36bb6350ea9a (diff) | |
ground->firstorder, cc-> congruence, CC final commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order')
| -rw-r--r-- | contrib/first-order/g_ground.ml4 | 14 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 3 |
2 files changed, 9 insertions, 8 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index 33e4107f6..d6f76a0a9 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -29,8 +29,8 @@ let ground_depth=ref 5 let _= let gdopt= { optsync=true; - optname="Ground Depth"; - optkey=SecondaryTable("Ground","Depth"); + optname="Firstorder Depth"; + optkey=SecondaryTable("Firstorder","Depth"); optread=(fun ()->Some !ground_depth); optwrite= (function @@ -65,7 +65,7 @@ let gen_ground_tac flag taco ext gl= qflag:=backup;result with e ->qflag:=backup;raise e -(* special for compatibility with old Intuition +(* special for compatibility with Intuition let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str @@ -81,12 +81,12 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) -TACTIC EXTEND Ground - [ "Ground" tactic_opt(t) "with" ne_reference_list(l) ] -> +TACTIC EXTEND Firstorder + [ "Firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ] -| [ "Ground" tactic_opt(t) "using" ne_preident_list(l) ] -> +| [ "Firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ] -| [ "Ground" tactic_opt(t) ] -> +| [ "Firstorder" tactic_opt(t) ] -> [ gen_ground_tac true (option_app eval_tactic t) Void ] END diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index c30c109c2..8f11089bf 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -279,7 +279,8 @@ let create_with_auto_hints l depth gl= let hdb= try Util.Stringmap.find dbname !searchtable - with Not_found-> error ("Ground: "^dbname^" : No such Hint database") in + with Not_found-> + error ("Firstorder: "^dbname^" : No such Hint database") in Hint_db.iter g hdb in List.iter h l; !seqref |