From 123c8683a25b34070d4874df4cdd9381d5ceac24 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 21 Mar 2008 16:20:59 +0000
Subject: Correct bug introduced in r10589, where we lost information that
 assumption types are types when type-checking them and necessary coercions
 were not inserted. Add empty_evar_defs definition in Evd and call the new
 helper function in constrintern that performs interpretation and gives back
 implicit argument information.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10706 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.ml  | 1 +
 pretyping/evd.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e044c17a99..2703e5ae0c 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -414,6 +414,7 @@ let create_evar_defs sigma =
 let create_goal_evar_defs sigma =
   let h = fold (fun mv _ l -> (mv,(dummy_loc,GoalEvar))::l) sigma [] in
   { evars=sigma; conv_pbs=[]; last_mods = []; history=h; metas=Metamap.empty }
+let empty_evar_defs = create_evar_defs empty
 let evars_of d = d.evars
 let evars_reset_evd evd d = {d with evars = evd}
 let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 7f5a4060b1..ebda685bd6 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -143,6 +143,7 @@ val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
 (* create an [evar_defs] with empty meta map: *)
 val create_evar_defs      : evar_map -> evar_defs
 val create_goal_evar_defs : evar_map -> evar_defs
+val empty_evar_defs : evar_defs
 val evars_of         : evar_defs -> evar_map
 val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
 
-- 
cgit v1.2.3