diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-14 09:52:25 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-14 09:52:25 +0000 |
| commit | 1b3efc6dc25be1bfde5fb7d2d39cc5c35e44a4d8 (patch) | |
| tree | 3f22240472bd260847f4b5b26581cfdfbc3e071a /tactics | |
| parent | 1674ab8bc0b76a1162928d0d9097c6a97486205d (diff) | |
Second step of integration of Program:
- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/contradiction.ml | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 |
3 files changed, 2 insertions, 3 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index f8cca076f..c4cf7b62f 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -22,7 +22,7 @@ open Glob_term let absurd c gls = let env = pf_env gls and sigma = project gls in - let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env + let _,j = Coercion.inh_coerce_to_sort dummy_loc env (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in let c = j.Environ.utj_val in (tclTHENS diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 9c0d5db2c..66c59ec36 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -588,7 +588,7 @@ let hResolve id c occ t gl = let t_raw = Detyping.detype true env_ids env_names t in let rec resolve_hole t_hole = try - Pretyping.Default.understand sigma env t_hole + Pretyping.understand sigma env t_hole with | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) -> resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d4a7be4ec..cf93a66cf 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,7 +44,6 @@ open Printer open Inductiveops open Syntax_def open Pretyping -open Pretyping.Default open Extrawit open Pcoq open Compat |