From 886a9c2fb25e32bd87b3fce38023b3e701134d23 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 27 Dec 2017 20:22:23 +0100
Subject: [econstr] Continue consolidation of EConstr API under `interp`.

This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.

The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.

We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.

In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.

Also, the new return type of `Pretyping.understand` should undergo
careful review.

We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.

Some TODOs are:

- impargs was calling whd_all, the Econstr equivalent can be either
  + Reductionops.whd_all [which does refolding and no sharing]
  + Reductionops.clos_whd_flags with all as a flag.
---
 pretyping/inductiveops.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 275a079d5d..33d674ff5d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -643,8 +643,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
 (* A function which checks that a term well typed verifies both
    syntactic conditions *)
 
-let control_only_guard env c =
-  let check_fix_cofix e c = match kind c with
+let control_only_guard env sigma c =
+  let check_fix_cofix e c =
+    match kind (EConstr.to_constr sigma c) with
     | CoFix (_,(_,_,_) as cofix) ->
       Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
@@ -653,6 +654,6 @@ let control_only_guard env c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    iter_constr_with_full_binders push_rel iter env c
+    iter_constr_with_full_binders sigma EConstr.push_rel iter env c
   in
   iter env c
-- 
cgit v1.2.3