Imported Upstream version 8.0pl2upstream/8.0pl2

7 files changed, 15 insertions, 15 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 423350d7..999bb651 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml,v 1.97.2.3 2004/07/16 19:30:48 herbelin Exp $ *)
+(* $Id: clenv.ml,v 1.97.2.4 2004/12/06 12:59:11 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -65,7 +65,7 @@ let exist_to_meta sigma (emap, c) =
     let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
     let n = new_meta() in
     metamap := (n, ty) :: !metamap;
-    mkMeta n in
+    mkCast (mkMeta n, ty) in
   let rec replace c =
     match kind_of_term c with
         Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 10e0004e..737fbea3 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: clenv.mli,v 1.32.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+(*i $Id: clenv.mli,v 1.32.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -102,9 +102,9 @@ val clenv_independent : wc clausenv -> metavariable list
 val clenv_missing : 'a clausenv -> metavariable list
 val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
   constr list -> wc clausenv -> wc clausenv
-(*
+(*i
 val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
-*)
+i*)
 val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
 val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d59ff835..ac4dd43a 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml,v 1.36.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+(* $Id: evar_refiner.ml,v 1.36.2.2 2004/08/03 21:37:27 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -178,6 +178,7 @@ let instantiate_pf_com n com pfts =
       List.nth (Evd.non_instantiated sigma) (n-1) 
     with Failure _ -> 
       error "not so many uninstantiated existential variables"
+      | Invalid_argument _ -> error "incorrect existential variable index"
   in 
   let c = Constrintern.interp_constr sigma (Evarutil.evar_env evd) com in     
   let wc' = w_Define sp c wc in
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index d7f393b3..d57e1b84 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evar_refiner.mli,v 1.28.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+(*i $Id: evar_refiner.mli,v 1.28.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -51,7 +51,7 @@ val w_const_value       : wc -> constant -> constr
 val w_defined_evar      : wc -> existential_key -> bool
 
 val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic
-(*
+(*i
 val instantiate_tac : tactic_arg list -> tactic
-*)
+i*)
 val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index bed1158d..f6f2082e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,4 +1,3 @@
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: refiner.mli,v 1.31.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
+(*i $Id: refiner.mli,v 1.31.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
 
 (*i*)
 open Term
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index d8d7319d..60a0a937 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacexpr.ml,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+(*i $Id: tacexpr.ml,v 1.33.2.2 2005/01/21 17:14:09 herbelin Exp $ i*)
 
 open Names
 open Topconstr
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 59b48da2..2990567e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacmach.mli,v 1.50.2.1 2004/07/16 19:30:50 herbelin Exp $ i*)
+(*i $Id: tacmach.mli,v 1.50.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -120,9 +120,9 @@ val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   evar_map -> pftreestate -> pftreestate
 
-(*
+(*i
 val vernac_tactic : string * tactic_arg list -> tactic
-*)
+i*)
 (*s The most primitive tactics. *)
 
 val refiner                   : rule -> tactic