- Propagation des evars non résolues vers les with_bindings; permet par exemple

  de résoudre des buts comme celui-ci :

  Record nat_retract : Type := 
    {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
  Goal nat_retract.
  exists (fun x => x) (fun x => x).

- Nouvelle tentative d'utilisation des types des metas/evars pour
  inférer de nouvelles instances de metas/evars; permet par exemple
  d'utiliser f_equal sans option with, mais aussi, avec la modif
  précédente, de résoudre des buts tels que

  Goal exists f:bool->Prop, f true = True.
  exists (fun x => True).

  [Les expériences passées avaient montré qu'en prenant en compte les
  types dans l'unification, on peut unifier trop tôt une evars à une
  mauvaise sorte; à défaut de mécanisme de prise en compte des problème
  d'unification avec sous-typage, on s'est interdit ici d'unifier des
  types qui sont des arités.]

- Tout les constr de tactic_expr deviennent des open_constr (même si seul
  with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.



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

5 files changed, 11 insertions, 15 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 8bba76007..db94fad14 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -49,7 +49,7 @@ let clenv_cast_meta clenv =
     match kind_of_term (strip_outer_cast u) with
       | Meta mv ->
 	  (try 
-            let b = Typing.meta_type clenv.env mv in
+            let b = Typing.meta_type clenv.evd mv in
 	    if occur_meta b then u
             else mkCast (mkMeta mv, DEFAULTcast, b)
 	  with Not_found -> u)
@@ -62,7 +62,7 @@ let clenv_cast_meta clenv =
 
 let clenv_refine clenv gls =
   tclTHEN
-    (tclEVARS (evars_of clenv.env)) 
+    (tclEVARS (evars_of clenv.evd)) 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 20ce39775..dfe0ab76d 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
 and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -73,7 +73,7 @@ and tactic_expr =
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -83,7 +83,7 @@ and atomic_tactic_expr =
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index f835e2ef4..c06aff7e1 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
 and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -108,7 +108,7 @@ and tactic_expr =
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -118,7 +118,7 @@ and atomic_tactic_expr =
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 43d5af159..03a32bab8 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -40,7 +40,7 @@ val abstract_operation : compound_rule -> tactic -> tactic
 val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
 val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
 val abstract_extended_tactic :
-  ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic
+  ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
 
 val refiner : rule -> tactic
 val frontier : transformation_tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b06ec2f49..c78e842ec 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -306,16 +306,12 @@ type glob_generic_argument = rawconstr_and_expr generic_argument
 type glob_red_expr =
     (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
 
-type closed_raw_generic_argument = constr_expr generic_argument
+type typed_generic_argument = Evd.open_constr generic_argument
 
 type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 
 type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 
-type open_generic_argument = Term.constr generic_argument
-
-type closed_generic_argument = Term.constr generic_argument
-
-type 'a closed_abstract_argument_type = ('a,Term.constr) abstract_argument_type
+type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
 type declaration_hook = Decl_kinds.strength -> global_reference -> unit