From 1de052a2415a70bf4e06be02bff60bee19c013cb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Apr 2003 12:23:39 +0000
Subject: Localisation des appels de tactiques définies sans arguments

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3922 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a2584773f2..0fd4130d24 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -245,7 +245,7 @@ type glob_tactic_expr =
      constr_pattern,
      evaluable_global_reference and_short_name or_var or_metanum,
      inductive or_var or_metanum,
-     ltac_constant or_var,
+     ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_tactic_expr
 
@@ -254,7 +254,7 @@ type glob_atomic_tactic_expr =
      constr_pattern,
      evaluable_global_reference and_short_name or_var or_metanum,
      inductive or_var or_metanum,
-     ltac_constant or_var,
+     ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_atomic_tactic_expr
 
@@ -263,7 +263,7 @@ type glob_tactic_arg =
      constr_pattern,
      evaluable_global_reference and_short_name or_var or_metanum,
      inductive or_var or_metanum,
-     ltac_constant or_var,
+     ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_tactic_arg
 
-- 
cgit v1.2.3