diff options
| author |  Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
| commit | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch) | |
| tree | a418d1edb3d53cdb4185b9719b7a70822cf5a24d /tactics | |
| parent | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff) | |
Imported Upstream version 8.3.pl2upstream/8.3.pl2
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
3 files changed, 7 insertions, 7 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index afd13b4c..66f15fbe 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: class_tactics.ml4 13902 2011-03-10 15:50:24Z msozeau $ *) open Pp open Util @@ -85,7 +85,7 @@ let evars_to_goals p evm = if goals = [] then None else let goals = List.rev goals in - let evm' = evars_reset_evd evm' evm in + let evm' = evars_reset_evd ~with_conv_pbs:false evm' evm in Some (goals, evm') (** Typeclasses instance search tactic / eauto *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 7a774cc9..411ccc0e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *) +(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *) open Pp open Util @@ -888,8 +888,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = with | Some w -> let w_type = type_of env sigma w in - if Evarconv.e_conv env evdref w_type a then - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + if Evarconv.e_cumul env evdref w_type a then + applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail]) else error "Cannot solve a unification problem." | None -> anomaly "Not enough components to build the dependent tuple" diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 569cf356..771047fd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *) +(* $Id: tactics.ml 13981 2011-04-08 16:59:26Z herbelin $ *) open Pp open Util @@ -3469,7 +3469,7 @@ let abstract_subproof id tac gl = try flush_and_check_evars (project gl) concl with Uninstantiated_evar _ -> error "\"abstract\" cannot handle existentials." in - let const = Pfedit.build_constant_by_tactic secsign concl + let const = Pfedit.build_constant_by_tactic id secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in |