diff options
| author | Matthieu Sozeau | 2014-09-17 00:03:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-17 00:10:03 +0200 |
| commit | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (patch) | |
| tree | e364fd928f247c249767ffb679b0265857327a6a /tactics/extratactics.ml4 | |
| parent | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (diff) | |
Revert specific syntax for primitive projections, avoiding ugly
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e4ba9a7ee5..41f8dc8dec 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -628,9 +628,8 @@ let hResolve id c occ t gl = let sigma = project gl in let env = Termops.clear_named_body id (pf_env gl) in let env_ids = Termops.ids_of_context env in - let env_names = Termops.names_of_rel_context env in - let c_raw = Detyping.detype true env_ids env_names sigma c in - let t_raw = Detyping.detype true env_ids env_names sigma t in + let c_raw = Detyping.detype true env_ids env sigma c in + let t_raw = Detyping.detype true env_ids env sigma t in let rec resolve_hole t_hole = try Pretyping.understand env sigma t_hole |