diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:03:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:10:03 +0200 |
| commit | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (patch) | |
| tree | e364fd928f247c249767ffb679b0265857327a6a /plugins/firstorder/instances.ml | |
| 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 'plugins/firstorder/instances.ml')
| -rw-r--r-- | plugins/firstorder/instances.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 2987ce60a..80576212f 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -118,7 +118,7 @@ let mk_open_instance id idc gl m t= let nid=(fresh_id avoid var_id gl) in (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype false [] [] evmap nt in + let rawt=Detyping.detype false [] env evmap nt in let rec raux n t= if Int.equal n 0 then t else match t with |