Clarification de l'ordre d'interprétation des variables dans ltac. En

particulier, TacCall(_,f,[]) est utilisé pour une référence à une
variable ltac ou une tactique et Reference(f) est utilisé pour une
référence à une variable ltac ou un constr (en passant,
standardisation de l'utilisation de constr: ou ltac: à setoid_ring).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10878 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 22 insertions, 22 deletions

diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 074f6ef79..601cabe00 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -32,7 +32,7 @@ Qed.
 Ltac natcst t :=
   match isnatcst t with
     true => constr:(N_of_nat t)
-  | _ => InitialRing.NotConstant
+  | _ => constr:InitialRing.NotConstant
   end.
 
 Ltac Ss_to_add f acc :=
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 4d96bec4c..c1fa963f2 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -667,17 +667,17 @@ End GEN_DIV.
    | (add rI (add rI rI)) => constr:3%positive
    | (mul (add rI rI) ?p) => (* 2p *)
        match inv_cst p with
-         NotConstant => NotConstant
-       | 1%positive => NotConstant (* 2*1 is not convertible to 2 *)
+         NotConstant => constr:NotConstant
+       | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *)
        | ?p => constr:(xO p)
        end
    | (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
        match inv_cst p with
-         NotConstant => NotConstant
-       | 1%positive => NotConstant
+         NotConstant => constr:NotConstant
+       | 1%positive => constr:NotConstant
        | ?p => constr:(xI p)
        end
-   | _ => NotConstant
+   | _ => constr:NotConstant
    end in
    inv_cst t.
 
@@ -687,7 +687,7 @@ End GEN_DIV.
      rO => constr:NwO
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => NotConstant
+       NotConstant => constr:NotConstant
      | ?p => constr:(Npos p::nil)
      end
    end.
@@ -699,7 +699,7 @@ End GEN_DIV.
      rO => constr:0%N
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => NotConstant
+       NotConstant => constr:NotConstant
      | ?p => constr:(Npos p)
      end
    end.
@@ -710,12 +710,12 @@ End GEN_DIV.
      rO => constr:0%Z
    | (opp ?p) =>
      match inv_gen_phi_pos rI add mul p with
-       NotConstant => NotConstant
+       NotConstant => constr:NotConstant
      | ?p => constr:(Zneg p)
      end
    | _ =>
      match inv_gen_phi_pos rI add mul t with
-       NotConstant => NotConstant
+       NotConstant => constr:NotConstant
      | ?p => constr:(Zpos p)
      end
    end.
@@ -731,7 +731,7 @@ Ltac inv_gen_phi rO rI cO cI t :=
   end.
 
 (* A simple tactic recognizing no constant *)
- Ltac inv_morph_nothing t := constr:(NotConstant).
+ Ltac inv_morph_nothing t := constr:NotConstant.
 
 Ltac coerce_to_almost_ring set ext rspec :=
   match type of rspec with
@@ -875,9 +875,9 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk :=
 (* Tactic for constant *)
 Ltac isnatcst t :=
   match t with
-    O => true
+    O => constr:true
   | S ?p => isnatcst p
-  | _ => false
+  | _ => constr:false
   end.
 
 Ltac isPcst t :=
@@ -887,7 +887,7 @@ Ltac isPcst t :=
   | xH => constr:true
   (* nat -> positive *)
   | P_of_succ_nat ?n => isnatcst n 
-  | _ => false
+  | _ => constr:false
   end.
 
 Ltac isNcst t :=
@@ -899,7 +899,7 @@ Ltac isNcst t :=
 
 Ltac isZcst t :=
   match t with
-    Z0 => true
+    Z0 => constr:true
   | Zpos ?p => isPcst p
   | Zneg ?p => isPcst p
   (* injection nat -> Z *)
@@ -907,7 +907,7 @@ Ltac isZcst t :=
   (* injection N -> Z *)
   | Z_of_N ?n => isNcst n
   (* *)
-  | _ => false
+  | _ => constr:false
   end.
 
 
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
index ae067a8a2..0ba519fde 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/contrib/setoid_ring/NArithRing.v
@@ -15,7 +15,7 @@ Set Implicit Arguments.
 Ltac Ncst t :=
   match isNcst t with
     true => t
-  | _ => NotConstant
+  | _ => constr:NotConstant
   end.
 
 Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]).
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
index 1a4e1cc75..d01b16258 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/contrib/setoid_ring/Ring.v
@@ -38,7 +38,7 @@ Ltac bool_cst t :=
   match t with
     true => constr:true
   | false => constr:false
-  | _ => NotConstant
+  | _ => constr:NotConstant
   end.
 
 Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]).
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 3cdce8da4..4a5b623b4 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -17,14 +17,14 @@ Set Implicit Arguments.
 Ltac Zcst t :=
   match isZcst t with
     true => t
-  | _ => NotConstant
+  | _ => constr:NotConstant
   end.
 
 Ltac isZpow_coef t :=
   match t with 
   | Zpos ?p => isPcst p
-  | Z0 => true
-  | _ => false
+  | Z0 => constr:true
+  | _ => constr:false
   end.
 
 Definition N_of_Z x :=
@@ -36,7 +36,7 @@ Definition N_of_Z x :=
 Ltac Zpow_tac t :=
  match isZpow_coef t with
  | true => constr:(N_of_Z t)
- | _ => constr:(NotConstant)
+ | _ => constr:NotConstant
  end.
 
 Ltac Zpower_neg :=