Intégration initiale du Cases

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

1 files changed, 4 insertions, 0 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c1313ee14..f55aaf69a 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -166,6 +166,10 @@ let restrict_hyps isevars c =
   end else 
     c
 
+let has_ise sigma t = 
+  try let _ = whd_ise sigma t in true
+  with UserError _ -> false
+
 (* We try to instanciate the evar assuming the body won't depend
  * on arguments that are not Rels or VARs, or appearing several times.
  *)