Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion de 'OpenConstr' constitué d'un terme avec Métas et d'une liste de types pour les métas

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

6 files changed, 24 insertions, 6 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5fce6b5956..7fb05a144c 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -515,11 +515,6 @@ let clenv_type_of ce c =
       (intmap_to_list ce.env)
   in
     Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c
-(*  Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c *)
-  (***
-  (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
-     (gLOB(w_hyps ce.hook)) c).uj_type
-  ***)
 
 let clenv_instance_type_of ce c =
   clenv_instance ce (mk_freelisted (clenv_type_of ce c))
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index b51866628f..30e5aeba2f 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -345,6 +345,8 @@ let ast_of_cvt_arg = function
   | Command c       -> ope ("COMMAND",[c])
   | Constr  c       -> 
     ope ("COMMAND",[ast_of_constr false (Global.env ()) c])
+  | OpenConstr  (_,c)       -> 
+    ope ("COMMAND",[ast_of_constr false (Global.env ()) c])
   | Constr_context _ ->
     anomalylabstrm "ast_of_cvt_arg" [<'sTR
       "Constr_context argument could not be used">]
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index d90d3a93a5..2a65d799b2 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -85,6 +85,7 @@ and validation = (proof_tree list -> proof_tree)
 and tactic_arg =
   | Command        of Coqast.t
   | Constr         of constr
+  | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
   | Integer        of int
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 99ebe330bd..1b4a1c60dc 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -88,6 +88,7 @@ and validation = (proof_tree list -> proof_tree)
 and tactic_arg =
   | Command        of Coqast.t
   | Constr         of constr
+  | OpenConstr     of ((int * constr) list * constr) (* constr with holes *)
   | Constr_context of constr
   | Identifier     of identifier
   | Integer        of int
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index ec3776c819..0d4d279d58 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -67,6 +67,10 @@ let pf_interp_constr gls c =
   let evc = project gls in 
   Astterm.interp_constr evc (sig_it gls).evar_env c
 
+let pf_interp_openconstr gls c =
+  let evc = project gls in 
+  Astterm.interp_openconstr evc (sig_it gls).evar_env c
+
 let pf_interp_type gls c =
   let evc = project gls in 
   Astterm.interp_type evc (sig_it gls).evar_env c
@@ -296,6 +300,7 @@ let overwriting_tactic = Refiner.overwriting_add_tactic
 
 type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
 
+(* Inutile ?! réécrit plus loin 
 let tactic_com tac t x = tac (pf_interp_constr x t) x
       
 let tactic_com_sort tac t x = tac (pf_interp_type x t) x
@@ -317,7 +322,7 @@ let tactic_com_bind_list_list tac args gl =
     (pf_interp_constr gl c,
      List.map (fun (b,c')->(b,pf_interp_constr gl c')) tl) in 
   tac (List.map translate args) gl
-
+*)
 
 (********************************************************)
 (* Functions for hiding the implementation of a tactic. *)
@@ -333,7 +338,11 @@ let overwrite_hidden_tactic s tac  =
   (fun args -> vernac_tactic(s,args))
 
 let tactic_com = 
+
   fun tac t x -> tac (pf_interp_constr x t) x
+
+let tactic_opencom = 
+  fun tac t x -> tac (pf_interp_openconstr x t) x
       
 let tactic_com_sort = 
   fun tac t x -> tac (pf_interp_type x t) x
@@ -406,6 +415,15 @@ let hide_constr_tactic s tac =
   add_tactic s tacfun;
   (fun c  -> vernac_tactic(s,[(Constr c)]))
 
+let hide_openconstr_tactic s tac =
+  let tacfun = function 
+    | [OpenConstr c] -> tac c
+    | [Command com] -> tactic_opencom tac com
+    | _ -> anomaly "hide_openconstr_tactic : neither OPENCONSTR nor COMMAND"
+  in 
+  add_tactic s tacfun;
+  (fun c  -> vernac_tactic(s,[(OpenConstr c)]))
+
 let hide_numarg_tactic s tac =
   let tacfun = (function [Integer n] -> tac n | _ -> assert false) in 
   add_tactic s tacfun;
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 9234d90a27..e2ae561eef 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -249,6 +249,7 @@ type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic)
 
 val hide_atomic_tactic  : string -> tactic -> tactic
 val hide_constr_tactic  : constr hide_combinator
+val hide_openconstr_tactic  : ((int * constr) list * constr) hide_combinator
 val hide_constrl_tactic : (constr list) hide_combinator
 val hide_numarg_tactic  : int hide_combinator
 val hide_ident_tactic   : identifier hide_combinator