From 6497f27021fec4e01f2182014f2bb1989b4707f9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 31 Jan 2005 14:34:14 +0000 Subject: Imported Upstream version 8.0pl2 --- proofs/clenv.ml | 4 ++-- proofs/clenv.mli | 6 +++--- proofs/evar_refiner.ml | 3 ++- proofs/evar_refiner.mli | 6 +++--- proofs/refiner.mli | 3 +-- proofs/tacexpr.ml | 2 +- proofs/tacmach.mli | 6 +++--- 7 files changed, 15 insertions(+), 15 deletions(-) (limited to 'proofs') 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 *) (* 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 -- cgit v1.2.3