summaryrefslogtreecommitdiff
path: root/contrib/first-order
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/first-order')
-rw-r--r--contrib/first-order/g_ground.ml410
-rw-r--r--contrib/first-order/rules.ml6
2 files changed, 8 insertions, 8 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 0970d5db..f9c4cea2 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_ground.ml4 7909 2006-01-21 11:09:18Z herbelin $ *)
+(* $Id: g_ground.ml4 8752 2006-04-27 19:37:33Z herbelin $ *)
open Formula
open Sequent
@@ -83,14 +83,14 @@ let normalize_evaluables=
TACTIC EXTEND firstorder
[ "firstorder" tactic_opt(t) "with" ne_reference_list(l) ] ->
- [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ]
+ [ gen_ground_tac true (option_map eval_tactic t) (Ids l) ]
| [ "firstorder" tactic_opt(t) "using" ne_preident_list(l) ] ->
- [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ]
+ [ gen_ground_tac true (option_map eval_tactic t) (Bases l) ]
| [ "firstorder" tactic_opt(t) ] ->
- [ gen_ground_tac true (option_app eval_tactic t) Void ]
+ [ gen_ground_tac true (option_map eval_tactic t) Void ]
END
TACTIC EXTEND gintuition
[ "gintuition" tactic_opt(t) ] ->
- [ gen_ground_tac false (option_app eval_tactic t) Void ]
+ [ gen_ground_tac false (option_map eval_tactic t) Void ]
END
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index f6653b82..6c51eda3 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.ml 7909 2006-01-21 11:09:18Z herbelin $ *)
+(* $Id: rules.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
open Util
open Names
@@ -211,6 +211,6 @@ let normalize_evaluables=
onAllClauses
(function
None->unfold_in_concl (Lazy.force defined_connectives)
- | Some (id,_,_)->
+ | Some ((_,id),_)->
unfold_in_hyp (Lazy.force defined_connectives)
- (id,[],Tacexpr.InHypTypeOnly))
+ (([],id),Tacexpr.InHypTypeOnly))