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

6 files changed, 17 insertions, 17 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 1b2f48f95c..2646a4c825 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -32,7 +32,7 @@ type argument_type =
   | SortArgType
   | ConstrArgType
   | ConstrMayEvalArgType
-  | QuantVarArgType
+  | QuantHypArgType
   | TacticArgType of int
   | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
@@ -124,9 +124,9 @@ let rawwit_ref = RefArgType
 let globwit_ref = RefArgType
 let wit_ref = RefArgType
 
-let rawwit_quant_hyp = QuantVarArgType
-let globwit_quant_hyp = QuantVarArgType
-let wit_quant_hyp = QuantVarArgType
+let rawwit_quant_hyp = QuantHypArgType
+let globwit_quant_hyp = QuantHypArgType
+let wit_quant_hyp = QuantHypArgType
 
 let rawwit_sort = SortArgType
 let globwit_sort = SortArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 50c8ab3e0b..d61245475c 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -71,7 +71,7 @@ VarArgType                     identifier               constr
 RefArgType                     reference                global_reference
 ConstrArgType                  constr_expr              constr
 ConstrMayEvalArgType           constr_expr may_eval     constr
-QuantVarArgType                quantified_hypothesis    quantified_hypothesis
+QuantHypArgType                quantified_hypothesis    quantified_hypothesis
 TacticArgType                  raw_tactic_expr          tactic
 OpenConstrArgType              constr_expr              open_constr
 ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
@@ -237,7 +237,7 @@ type argument_type =
   | SortArgType
   | ConstrArgType
   | ConstrMayEvalArgType
-  | QuantVarArgType
+  | QuantHypArgType
   | TacticArgType of int
   | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 331df4c709..d1f82c1d99 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -29,7 +29,7 @@ let rec make_rawwit loc = function
   | SortArgType -> <:expr< Genarg.rawwit_sort >>
   | ConstrArgType -> <:expr< Genarg.rawwit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
-  | QuantVarArgType -> <:expr< Genarg.rawwit_quant_hyp >>
+  | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
   | TacticArgType n -> <:expr< Genarg.rawwit_tactic $mlexpr_of_int n$ >>
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
   | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
@@ -52,7 +52,7 @@ let rec make_globwit loc = function
   | IdentArgType -> <:expr< Genarg.globwit_ident >>
   | VarArgType -> <:expr< Genarg.globwit_var >>
   | RefArgType -> <:expr< Genarg.globwit_ref >>
-  | QuantVarArgType -> <:expr< Genarg.globwit_quant_hyp >>
+  | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
   | SortArgType -> <:expr< Genarg.globwit_sort >>
   | ConstrArgType -> <:expr< Genarg.globwit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
@@ -78,7 +78,7 @@ let rec make_wit loc = function
   | IdentArgType -> <:expr< Genarg.wit_ident >>
   | VarArgType -> <:expr< Genarg.wit_var >>
   | RefArgType -> <:expr< Genarg.wit_ref >>
-  | QuantVarArgType -> <:expr< Genarg.wit_quant_hyp >>
+  | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
   | SortArgType -> <:expr< Genarg.wit_sort >>
   | ConstrArgType -> <:expr< Genarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9803c00314..8360e280a4 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -141,7 +141,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
   | ConstrMayEvalArgType ->
       pr_arg (pr_may_eval prc prlc prref)
         (out_gen rawwit_constr_may_eval x)
-  | QuantVarArgType ->
+  | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x)
@@ -184,7 +184,7 @@ let rec pr_glob_generic prc prlc prtac x =
   | ConstrMayEvalArgType ->
       pr_arg (pr_may_eval prc prlc
         (pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
-  | QuantVarArgType ->
+  | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr 
@@ -229,7 +229,7 @@ let rec pr_generic prc prlc prtac x =
   | ConstrArgType -> pr_arg prc (out_gen wit_constr x)
   | ConstrMayEvalArgType ->
       pr_arg prc (out_gen wit_constr_may_eval x)
-  | QuantVarArgType ->
+  | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d28b36924b..f8172ac6e1 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -173,7 +173,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
-  | Genarg.QuantVarArgType -> <:expr< Genarg.QuantVarArgType >>
+  | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
   | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
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))