From 44c8ded85ffc7777562cd6fcfbdf34e332461fad Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Feb 2001 15:10:13 +0000
Subject: Prise en compte noms longs dans SuperAuto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1391 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_trees.ml | 1 +
 proofs/proof_type.ml  | 1 +
 proofs/proof_type.mli | 1 +
 3 files changed, 3 insertions(+)

(limited to 'proofs')

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 46c4e907d9..8a655b3da2 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -389,6 +389,7 @@ let ast_of_cvt_redexp = function
 (* Gives the ast corresponding to a tactic argument *)
 let ast_of_cvt_arg = function
   | Identifier id   -> nvar (string_of_id id) 
+  | Qualid qid      -> nvar (string_of_qualid qid) 
   | Quoted_string s -> str s
   | Integer n       -> num n 
   | Command c       -> ope ("COMMAND",[c])
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e1cc05873b..319b7ff4f9 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -88,6 +88,7 @@ and tactic_arg =
   | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
+  | Qualid         of qualid
   | Integer        of int
   | Clause         of identifier list
   | Bindings       of Coqast.t substitution
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 7025f450a1..e49faeb58e 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -120,6 +120,7 @@ and tactic_arg =
   | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
+  | Qualid         of qualid
   | Integer        of int
   | Clause         of identifier list
   | Bindings       of Coqast.t substitution
-- 
cgit v1.2.3