From 34e86e839be251717db96f1f5969d7724ab43097 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 02:45:54 +0100
Subject: Hints API using EConstr.

---
 engine/evarutil.ml  | 6 ++++--
 engine/evarutil.mli | 2 +-
 engine/termops.ml   | 5 +++--
 engine/termops.mli  | 2 +-
 4 files changed, 9 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 35fe9cf668..8b75d8242f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -187,7 +187,9 @@ let is_ground_env = memo is_ground_env
 
 exception NoHeadEvar
 
-let head_evar =
+let head_evar sigma c =
+  (** FIXME: this breaks if using evar-insensitive code *)
+  let c = EConstr.Unsafe.to_constr c in
   let rec hrec c = match kind_of_term c with
     | Evar (evk,_)   -> evk
     | Case (_,_,c,_) -> hrec c
@@ -196,7 +198,7 @@ let head_evar =
     | Proj (p, c)    -> hrec c
     | _              -> raise NoHeadEvar
   in
-  hrec
+  hrec c
 
 (* Expand head evar if any (currently consider only applications but I
    guess it should consider Case too) *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ad3851ea31..1b592b7905 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -88,7 +88,7 @@ val non_instantiated : evar_map -> evar_info Evar.Map.t
 
 (** [head_evar c] returns the head evar of [c] if any *)
 exception NoHeadEvar
-val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
+val head_evar : evar_map -> EConstr.constr -> existential_key (** may raise NoHeadEvar *)
 
 (* Expand head evar if any *)
 val whd_head_evar :  evar_map -> EConstr.constr -> EConstr.constr
diff --git a/engine/termops.ml b/engine/termops.ml
index ef7cdc38b5..7c89f190f2 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -263,9 +263,10 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
   (* Removed trailing extra implicit arguments, what improves compatibility
      for constants with recently added maximal implicit arguments *)
   | App (f,args) when EConstr.isEvar sigma (Array.last args) ->
+      let open EConstr in
       drop_extra_implicit_args sigma
-	(EConstr.mkApp (f,fst (Array.chop (Array.length args - 1) args)))
-  | _ -> EConstr.Unsafe.to_constr c
+	(mkApp (f,fst (Array.chop (Array.length args - 1) args)))
+  | _ -> c
 
 (* Get the last arg of an application *)
 let last_arg sigma c = match EConstr.kind sigma c with
diff --git a/engine/termops.mli b/engine/termops.mli
index 72c0cedda3..a865c80fbb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -96,7 +96,7 @@ val iter_constr_with_full_binders :
 (**********************************************************************)
 
 val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t
-val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> constr
+val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> EConstr.constr
 
 (** occur checks *)
 
-- 
cgit v1.2.3