From 099fb1b4c5084bb899e4910e42c971cdfa81e1aa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 26 Dec 2005 17:08:16 +0000
Subject: Petite correction nom QuantHypArgType suite suppression traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7739 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5f2baf8f8c..18b7604fb1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -854,7 +854,7 @@ and intern_genarg ist x =
   | ConstrMayEvalArgType ->
       in_gen globwit_constr_may_eval 
         (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
-  | QuantVarArgType ->
+  | QuantHypArgType ->
       in_gen globwit_quant_hyp
         (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
   | RedExprArgType ->
@@ -1609,7 +1609,7 @@ and interp_genarg ist goal x =
       in_gen wit_constr (pf_interp_constr ist goal (out_gen globwit_constr x))
   | ConstrMayEvalArgType ->
       in_gen wit_constr_may_eval (interp_constr_may_eval ist goal (out_gen globwit_constr_may_eval x))
-  | QuantVarArgType ->
+  | QuantHypArgType ->
       in_gen wit_quant_hyp
         (interp_declared_or_quantified_hypothesis ist goal
           (out_gen globwit_quant_hyp x))
@@ -1828,7 +1828,7 @@ and interp_atomic ist gl = function
     | TacticArgType n -> 
 	val_interp ist gl (out_gen (globwit_tactic n) x)
     | StringArgType | BoolArgType
-    | QuantVarArgType | RedExprArgType 
+    | QuantHypArgType | RedExprArgType 
     | OpenConstrArgType _ | ConstrWithBindingsArgType | BindingsArgType 
     | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
@@ -2121,7 +2121,7 @@ and subst_genarg subst (x:glob_generic_argument) =
       in_gen globwit_constr (subst_rawconstr subst (out_gen globwit_constr x))
   | ConstrMayEvalArgType ->
       in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
-  | QuantVarArgType ->
+  | QuantHypArgType ->
       in_gen globwit_quant_hyp
         (subst_declared_or_quantified_hypothesis subst 
           (out_gen globwit_quant_hyp x))
-- 
cgit v1.2.3