Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 14 insertions, 9 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 262214c3a7..16227d4ba6 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -56,9 +56,9 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar
 let tj_nf_evar = Pretype_errors.tj_nf_evar
 
 let nf_evar_info evc info =
-  { evar_concl = Reductionops.nf_evar evc info.evar_concl;
-    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
-    evar_body = info.evar_body}
+  { info with 
+      evar_concl = Reductionops.nf_evar evc info.evar_concl;
+      evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
 
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 8b7f82cc33..5a353978d4 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -30,7 +30,8 @@ type evar_body =
 type evar_info = {
   evar_concl : constr;
   evar_hyps : named_context_val;
-  evar_body : evar_body}
+  evar_body : evar_body;
+  evar_extra : Dyn.t option}
 
 let evar_context evi = named_context_of_val evi.evar_hyps
 
@@ -64,9 +65,8 @@ let define evd ev body =
     try find evd ev
     with Not_found -> error "Evd.define: cannot define undeclared evar" in
   let newinfo =
-    { evar_concl = oldinfo.evar_concl;
-      evar_hyps = oldinfo.evar_hyps;
-      evar_body = Evar_defined body} in
+    { oldinfo with
+      evar_body = Evar_defined body } in
   match oldinfo.evar_body with
     | Evar_empty -> Evarmap.add ev newinfo evd
     | _ -> anomaly "Evd.define: cannot define an isevar twice"
@@ -393,7 +393,10 @@ let evar_define sp body isevars =
 let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
   { evd with
     evars = add evd.evars evn
-      {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty};
+      {evar_hyps=hyps; 
+       evar_concl=ty; 
+       evar_body=Evar_empty; 
+       evar_extra=None};
     history = (evn,src)::evd.history }
 
 let is_defined_evar isevars (n,_) = is_defined isevars.evars n
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 6481ff2012..601c6c8b03 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -32,7 +32,8 @@ type evar_body =
 type evar_info = {
   evar_concl : constr;
   evar_hyps : Environ.named_context_val;
-  evar_body : evar_body}
+  evar_body : evar_body;
+  evar_extra : Dyn.t option}
 
 val eq_evar_info : evar_info -> evar_info -> bool
 val evar_context : evar_info -> named_context
@@ -94,6 +95,7 @@ type 'a freelisted = {
   rebus : 'a;
   freemetas : Metaset.t }
 
+val metavars_of : constr -> Metaset.t
 val mk_freelisted : constr -> constr freelisted
 val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted