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

12 files changed, 164 insertions, 183 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 8991286092..080fd7b21c 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -524,12 +524,20 @@ let _ =
 (*********************************************************************)
 (* V6 compat: Functions before in ex-trad                            *)
 
-(* Endless^H^H^H^H^H^H^HShort list of alternative ways to call pretyping *)
+(* Functions to parse and interpret constructions *)
 
 let interp_constr sigma env c =
-  ise_resolve sigma env (interp_rawconstr sigma env c)
+  understand sigma env (interp_rawconstr sigma env c)
+
+let interp_openconstr sigma env c =
+  understand_gen_tcc sigma env [] [] None (interp_rawconstr sigma env c)
+
+let interp_casted_openconstr sigma env c typ =
+  understand_gen_tcc sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
+
 let interp_type sigma env   c =
-  ise_resolve_type sigma env (interp_rawconstr sigma env c)
+  understand_type sigma env (interp_rawconstr sigma env c)
+
 let interp_sort = function
   | Node(loc,"PROP", []) -> Prop Null
   | Node(loc,"SET", [])  -> Prop Pos
@@ -537,40 +545,36 @@ let interp_sort = function
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
 let judgment_of_rawconstr sigma env c =
-  ise_infer sigma env (interp_rawconstr sigma env c)
+  understand_judgment sigma env (interp_rawconstr sigma env c)
 
 let type_judgment_of_rawconstr sigma env c =
-  ise_infer_type sigma env (interp_rawconstr sigma env c)
+  understand_type_judgment sigma env (interp_rawconstr sigma env c)
 
 (*To retype a list of key*constr with undefined key*)
 let retype_list sigma env lst=
   List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst;;
 
-(*Interprets a constr according to two lists of instantiations (variables and
-  metas)*)
-let interp_constr1 sigma env lvar lmeta com =
+(* Note: typ is retyped *)
+
+let interp_casted_gen_constr1 sigma env lvar lmeta exptyp com =
   let c =
     interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst
       x)) lvar) com
   and rtype=fun lst -> retype_list sigma env lst in
-  try
-    ise_resolve2 sigma env (rtype lvar) (rtype lmeta) c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
+  understand_gen sigma env (rtype lvar) (rtype lmeta) exptyp c;;
 
-(* Note: typ is retyped *)
-
-let interp_casted_constr sigma env com typ = 
-  ise_resolve_casted sigma env typ (interp_rawconstr sigma env com)
+(*Interprets a constr according to two lists of instantiations (variables and
+  metas)*)
+let interp_constr1 sigma env lvar lmeta com =
+  interp_casted_gen_constr1 sigma env lvar lmeta None com
 
 (*Interprets a casted constr according to two lists of instantiations
   (variables and metas)*)
 let interp_casted_constr1 sigma env lvar lmeta com typ =
-  let c =
-    interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst
-      x)) lvar) com
-  and rtype=fun lst -> retype_list sigma env lst in 
-  ise_resolve_casted_gen true sigma env (rtype lvar) (rtype lmeta) typ c;;
+  interp_casted_gen_constr1 sigma env lvar lmeta (Some typ) com
+
+let interp_casted_constr sigma env com typ = 
+  understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env com)
 
 (* To process patterns, we need a translation from AST to term
    without typing at all. *)
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 95810a36f0..3274cf6f4f 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -19,6 +19,11 @@ val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
 val interp_type          : 'a evar_map -> env -> Coqast.t -> constr
 val interp_sort          : Coqast.t -> sorts
 
+val interp_openconstr    :
+  'a evar_map -> env -> Coqast.t -> (int * constr) list * constr
+val interp_casted_openconstr    :
+  'a evar_map -> env -> Coqast.t -> constr -> (int * constr) list * constr
+
 val judgment_of_rawconstr : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
 val type_judgment_of_rawconstr :
   'a evar_map -> env -> Coqast.t -> unsafe_type_judgment
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bb396f528a..6b698e28f5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -167,9 +167,6 @@ let pretype_id loc env lvar id =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let trad_metamap = ref []
-let trad_nocheck = ref false
-
 let pretype_ref pretype loc isevars env lvar = function
 | RVar id -> pretype_id loc env lvar id
 
@@ -177,7 +174,16 @@ let pretype_ref pretype loc isevars env lvar = function
     let cst = (sp,Array.map pretype ctxt) in
     make_judge (mkConst cst) (type_of_constant env !isevars cst)
 
-| REVar (sp,ctxt) -> error " Not able to type terms with dependent subgoals"
+| REVar (sp,ctxt) ->
+    let ev = (sp,Array.map pretype ctxt) in
+    let body = 
+      if Evd.is_defined !isevars sp then
+	existential_value !isevars ev
+      else
+	mkEvar ev
+    in
+    let typ = existential_type !isevars ev in
+    make_judge body (Retyping.get_assumption_of env !isevars typ)
 
 | RInd (ind_sp,ctxt) ->
     let ind = (ind_sp,Array.map pretype ctxt) in
@@ -211,14 +217,8 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
        List.assoc n lmeta
      with
         Not_found ->
-          let metaty =
-            try List.assoc n !trad_metamap
-            with Not_found ->
-	    (* Tester si la référence est castée *)
-	      user_err_loc (loc,"pretype",
-	        [< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >])
-	  in
-          { uj_val= mkMeta n; uj_type = outcast_type metaty })
+	  user_err_loc (loc,"pretype",
+			[< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >]))
 
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
@@ -272,7 +272,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       (rng_tycon,cj::jl)  in
     let jl = List.rev (snd (List.fold_left apply_one_arg
 			      (mk_tycon (body_of_type j.uj_type),[]) args)) in
-    inh_apply_rel_list !trad_nocheck loc env isevars jl j tycon
+    inh_apply_rel_list false loc env isevars jl j tycon
 
 | RBinder(loc,BLambda,name,c1,c2)      ->
     let (dom,rng) = split_tycon loc env isevars tycon in
@@ -399,56 +399,58 @@ and pretype_type valcon env isevars lvar lmeta = function
 	  error_unexpected_type_loc (loc_of_rawconstr c) env tj.uj_val v
 
 
-let unsafe_infer tycon nocheck isevars metamap env lvar lmeta constr =
-  trad_metamap := metamap;
-  trad_nocheck := nocheck;
+let unsafe_infer tycon isevars env lvar lmeta constr =
   reset_problems ();
   pretype tycon env isevars lvar lmeta constr
 
-
-let unsafe_infer_type valcon nocheck isevars metamap env lvar lmeta constr =
-  trad_metamap := metamap;
-  trad_nocheck := nocheck;
+let unsafe_infer_type valcon isevars env lvar lmeta constr =
   reset_problems ();
   pretype_type valcon env isevars lvar lmeta constr
 
+(* If fail_evar is false, [process_evars] turns unresolved Evar that
+   were not in initial sigma into Meta's; otherwise it fail on the first
+   unresolved Evar not already in the initial sigma
+   Rem: Does a side-effect on reference metamap *)
 (* [fail_evar] says how to process unresolved evars:
  *   true -> raise an error message
  *   false -> convert them into new Metas (casted with their type)
  *)
-let process_evars fail_evar env sigma =
-  (if fail_evar then
-     try whd_ise env sigma
-     with Uninstantiated_evar n ->
-          errorlabstrm "whd_ise"
-            [< 'sTR"There is an unknown subterm I cannot solve" >]
-   else whd_ise1_metas env sigma)
-
-(*
-let j_apply f env sigma j =
-  { uj_val= local_strong (under_outer_cast (f env sigma)) j.uj_val;
-    uj_type= typed_app (strong f env sigma) j.uj_type }
-*)
-let j_apply f env sigma j =
-  { uj_val= strong f env sigma j.uj_val;
-    uj_type= typed_app (strong f env sigma) j.uj_type }
-
-let utj_apply f env sigma j =
-  let under_outer_cast f env sigma c = match kind_of_term c with
-    | IsCast (b,t) -> mkCast (f env sigma b,f env sigma t)
-    | _ -> f env sigma c in
-  { utj_val = strong (under_outer_cast f) env sigma j.utj_val;
-    utj_type = j.utj_type }
-
+let process_evars fail_evar initial_sigma sigma metamap c =
+  let rec proc_rec c =
+    match kind_of_term c with
+      | IsEvar (ev,args as k) when Evd.in_dom sigma ev ->
+	  if Evd.is_defined sigma ev then
+      	    proc_rec (existential_value sigma k)
+	  else
+	    if Evd.in_dom initial_sigma ev then
+	      c
+	    else
+	      if fail_evar then
+		errorlabstrm "whd_ise"
+		  [< 'sTR"There is an unknown subterm I cannot solve" >]
+	      else
+		let n = new_meta () in
+		metamap := (n, existential_type sigma k) :: !metamap;
+		mkMeta n
+      | _ -> map_constr proc_rec c      
+  in
+  proc_rec c
+ 
 (* TODO: comment faire remonter l'information si le typage a resolu des
        variables du sigma original. il faudrait que la fonction de typage
        retourne aussi le nouveau sigma...
 *)
 
+type meta_map = (int * unsafe_judgment) list
+type var_map = (identifier * unsafe_judgment) list
+
 let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
   let isevars = ref sigma in
-  let j = unsafe_infer (mk_tycon typ) false isevars [] env lvar lmeta c in
-  (j_apply (fun _ -> process_evars fail_evar) env !isevars j).uj_val
+  let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
+  let metamap = ref [] in
+  let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
+  let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+  !metamap, {uj_val = v; uj_type = t }
 
 let ise_resolve_casted sigma env typ c =
   ise_resolve_casted_gen true sigma env [] [] typ c
@@ -456,55 +458,41 @@ let ise_resolve_casted sigma env typ c =
 (* Raw calls to the unsafe inference machine: boolean says if we must fail
    on unresolved evars, or replace them by Metas; the unsafe_judgment list
    allows us to extend env with some bindings *)
-let ise_infer_gen fail_evar sigma metamap env lvar lmeta c =
+let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
+  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
   let isevars = ref sigma in
-  let j = unsafe_infer empty_tycon false isevars metamap env lvar lmeta c in
-  j_apply (fun _ -> process_evars fail_evar) env !isevars j
+  let j = unsafe_infer tycon isevars env lvar lmeta c in
+  let metamap = ref [] in
+  let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
+  let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+  !metamap, {uj_val = v; uj_type = t }
 
-let ise_infer_type_gen fail_evar sigma metamap env c =
+let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
   let isevars = ref sigma in
-  let j = unsafe_infer_type empty_valcon false isevars metamap env [] [] c in
+  let j = unsafe_infer_type empty_valcon isevars env lvar lmeta c in
   let tj = inh_ass_of_j env isevars j in
-  utj_apply (fun _ -> process_evars fail_evar) env !isevars tj
-
-let ise_infer_nocheck sigma metamap env c =
-  let isevars = ref sigma in
-  let j = unsafe_infer empty_tycon true isevars metamap env [] [] c in
-  j_apply (fun _ -> process_evars true) env !isevars j
+  let metamap = ref [] in
+  let v = process_evars fail_evar sigma !isevars metamap tj.utj_val in
+  !metamap, {utj_val = v; utj_type = tj.utj_type }
 
-let ise_infer sigma env c =
-  ise_infer_gen true sigma [] env [] [] c
+let understand_judgment sigma env c =
+  snd (ise_infer_gen true sigma env [] [] None c)
 
-let ise_infer_type sigma env c =
-  ise_infer_type_gen true sigma [] env c
+let understand_type_judgment sigma env c =
+  snd (ise_infer_type_gen true sigma env [] [] c)
 
-let ise_resolve sigma env c =
-  (ise_infer_gen true sigma [] env [] [] c).uj_val
+let understand sigma env c =
+  let _, c = ise_infer_gen true sigma env [] [] None c in
+  c.uj_val
 
-let ise_resolve_type sigma env c =
-  (ise_infer_type_gen true sigma [] env c).utj_val
-
-let ise_resolve2 sigma env lmeta lvar c =
-  (ise_infer_gen true sigma [] env lmeta lvar c).uj_val;;
-
-(* Keeping universe constraints *)
-(*
-let fconstruct_type_with_univ_sp sigma sign sp c =
-  with_universes
-    (Mach.fexecute_type sigma sign) (sp,initial_universes,c) 
+let understand_type sigma env c =
+  let _,c = ise_infer_type_gen true sigma env [] [] c in
+  c.utj_val
 
+let understand_gen sigma env lvar lmeta exptyp c =
+  let _, c = ise_infer_gen true sigma env lvar lmeta exptyp c in
+  c.uj_val
 
-let fconstruct_with_univ_sp sigma sign sp c =
-  with_universes
-    (Mach.fexecute sigma sign) (sp,initial_universes,c) 
-
-
-let infconstruct_type_with_univ_sp sigma (sign,fsign) sp c =
-  with_universes
-    (Mach.infexecute_type sigma (sign,fsign)) (sp,initial_universes,c) 
-
-
-let infconstruct_with_univ_sp sigma (sign,fsign) sp c =
-  with_universes
-    (Mach.infexecute sigma (sign,fsign)) (sp,initial_universes,c) 
-*)
+let understand_gen_tcc sigma env lvar lmeta exptyp c =
+  let metamap, c = ise_infer_gen false sigma env lvar lmeta exptyp c in
+  metamap, c.uj_val
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 099f75140a..04995dcb59 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -11,65 +11,43 @@ open Rawterm
 open Evarutil
 (*i*)
 
-(* Raw calls to the inference machine of Trad: boolean says if we must fail
-   on unresolved evars, or replace them by Metas ; the [unsafe_judgment] list
-   allows us to extend env with some bindings *)
-val ise_infer_gen : bool -> 'a evar_map -> (int * constr) list ->
-  env -> (identifier * unsafe_judgment) list ->
-  (int * unsafe_judgment) list -> rawconstr -> unsafe_judgment
+type meta_map = (int * unsafe_judgment) list
+type var_map = (identifier * unsafe_judgment) list
 
-(* Standard call to get an unsafe judgment from a rawconstr, resolving
-   implicit args *)
-val ise_infer : 'a evar_map -> env -> rawconstr -> unsafe_judgment
+(* Generic call to the interpreter from rawconstr to constr, failing
+   unresolved holes in the rawterm cannot be instantiated.
 
-(* Standard call to get an unsafe type judgment from a rawconstr, resolving
-   implicit args *)
-val ise_infer_type : 'a evar_map -> env -> rawconstr -> unsafe_type_judgment
+   In [understand_gen sigma env varmap metamap typopt raw],
 
-(* Standard call to get a constr from a rawconstr, resolving implicit args *)
-val ise_resolve      : 'a evar_map -> env -> rawconstr -> constr
+   sigma : initial set of existential variables (typically dependent subgoals)
+   varmap : partial subtitution of variables (used for the tactic language)
+   metamap : partial subtitution of meta (used for the tactic language)
+   typopt : is not None, this is the expected type for raw (used to define evars)
+*)
+val understand_gen :
+  'a evar_map -> env -> var_map -> meta_map 
+    -> expected_type:(constr option) -> rawconstr -> constr
 
-(* Idem but the rawconstr is intended to be a type *)
-val ise_resolve_type : 'a evar_map -> env -> rawconstr -> constr
 
-val ise_resolve2 : 'a evar_map -> env -> (identifier * unsafe_judgment) list ->
-  (int * unsafe_judgment) list -> rawconstr -> constr
+(* Generic call to the interpreter from rawconstr to constr, turning
+   unresolved holes into metas. Returns also the typing context of
+   these metas. Work as [understand_gen] for the rest. *)
+val understand_gen_tcc :
+  'a evar_map -> env -> var_map -> meta_map 
+    -> constr option -> rawconstr -> (int * constr) list * constr
 
-val ise_resolve_casted_gen :
-  bool -> 'a evar_map -> env -> (identifier * unsafe_judgment) list ->
-    (int * unsafe_judgment) list -> constr -> rawconstr -> constr
-val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
+(* Standard call to get a constr from a rawconstr, resolving implicit args *)
+val understand : 'a evar_map -> env -> rawconstr -> constr
 
-(* progmach.ml tries to type ill-typed terms: does not perform the conversion
- * test in application.
- *)
-val ise_infer_nocheck : 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> unsafe_judgment
+(* Idem but the rawconstr is intended to be a type *)
+val understand_type : 'a evar_map -> env -> rawconstr -> constr
 
-(* Typing with Trad, and re-checking with Mach *)
-(*i
-val infconstruct_type :
-  'c evar_map -> (env * env) ->
-    Coqast.t -> typed_type * information
-val infconstruct :
-  'c evar_map -> (env * env) ->
-    Coqast.t -> unsafe_judgment * information
+(* Idem but returns the judgment of the understood term *)
+val understand_judgment : 'a evar_map -> env -> rawconstr -> unsafe_judgment
 
-(* Typing, re-checking with universes constraints *)
-val fconstruct_with_univ :
-  'c evar_map -> env -> Coqast.t -> unsafe_judgment
-val fconstruct_with_univ_sp : 'c evar_map -> env
-  -> section_path -> constr -> Impuniv.universes * unsafe_judgment
-val fconstruct_type_with_univ_sp : 'c evar_map -> env
-  -> section_path -> constr -> Impuniv.universes * typed_type
-val infconstruct_with_univ_sp :
-  'c evar_map -> (env * env)
-  -> section_path -> constr -> Impuniv.universes * (unsafe_judgment * information)
-val infconstruct_type_with_univ_sp :
-  'c evar_map -> (env * env)
-  -> section_path -> constr 
-  -> Impuniv.universes * (typed_type * information)
-i*)
+(* Idem but returns the judgment of the understood type *)
+val understand_type_judgment : 'a evar_map -> env -> rawconstr 
+  -> unsafe_type_judgment
 
 (*i*)
 (* Internal of Pretyping...
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
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 75f22c4ffc..53cced1616 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -269,24 +269,12 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 
 (* Et finalement la tactique refine elle-même : *)
 
-let refine c gl =
+let refine (lmeta,c) gl =
   let env = pf_env gl in
   let th = compute_metamap env c in
   tcc_aux th gl
 
-let refine_tac = Tacmach.hide_constr_tactic "Refine" refine
-
-let my_constr_of_com_casted sigma env com typ = 
-  let rawc = Astterm.interp_rawconstr sigma env com in
-  Printf.printf "ICI\n"; flush stdout;
-  let c = Pretyping.ise_resolve_casted_gen false sigma env [] [] typ rawc in
-  Printf.printf "LA\n"; flush stdout;
-  c
-  (**
-  let cc = mkCast (nf_ise1 sigma c, nf_ise1 sigma typ) in
-  try (unsafe_machine env sigma cc).uj_val
-  with e -> Stdpp.raise_with_loc (Ast.loc com) e
-  **)
+let refine_tac = Tacmach.hide_openconstr_tactic "Refine" refine
 
 open Proof_type
 
@@ -294,8 +282,8 @@ let dyn_tcc args gl = match args with
   | [Command com]  ->
       let env = pf_env gl in
       refine
-	(my_constr_of_com_casted (project gl) env com (pf_concl gl)) gl
-  | [Constr c] -> 
+	(Astterm.interp_casted_openconstr (project gl) env com (pf_concl gl)) gl
+  | [OpenConstr c] -> 
       refine c gl
   | _ -> assert false
 
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 0277770374..50b08265f4 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -4,5 +4,5 @@
 open Term
 open Tacmach
 
-val refine : constr -> tactic
-val refine_tac : constr -> tactic
+val refine : (int * constr) list * constr -> tactic
+val refine_tac : (int * constr) list * constr -> tactic