From b61d0df2899f5de9c20ee4a2c4b79deb0714b162 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Apr 2007 09:34:32 +0000
Subject: Ajout de la possibilité d'utiliser les evars dans apply_in et
 elim_in. Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
 "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 5 +++--
 proofs/tacmach.ml | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 633a9a42d3..14794086ab 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -21,6 +21,7 @@ type 'a or_metaid = AI of 'a | MetaId of loc * string
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag = bool      (* true = lazy             false = eager *)
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 
 type raw_red_flag =
   | FBeta
@@ -122,7 +123,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
   | TacVmCastNoCheck of 'constr
-  | TacApply of 'constr with_bindings
+  | TacApply of evars_flag * 'constr with_bindings
   | TacElim of 'constr with_bindings * 'constr with_bindings option
   | TacElimType of 'constr
   | TacCase of 'constr with_bindings
@@ -184,7 +185,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* Equality and inversion *)
-  | TacRewrite of bool * 'constr with_bindings * 'id gclause
+  | TacRewrite of bool * evars_flag * 'constr with_bindings * 'id gclause
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 06178324d9..2049eb0f6a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -235,7 +235,7 @@ let thin l             = with_check (thin_no_check l)
 let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
 let rename_hyp id id'  = with_check (rename_hyp_no_check id id')
-    
+
 (* Pretty-printers *)
 
 open Pp
-- 
cgit v1.2.3