- Documentation of the Program tactics.

- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.



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

1 files changed, 7 insertions, 0 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 26df8f793..5da0a1a99 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -408,6 +408,13 @@ let is_undefined_evar isevars c = match kind_of_term c with
   | Evar ev -> not (is_defined_evar isevars ev)
   | _ -> false
 
+let undefined_evars isevars = 
+  let evd = 
+    fold (fun ev evi sigma -> if evi.evar_body = Evar_empty then 
+	    add sigma ev evi else sigma) 
+      isevars.evars empty
+  in 
+    { isevars with evars = evd }
 
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)