From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

---
 plugins/cc/ccalgo.ml | 7 +++----
 plugins/cc/cctac.ml  | 4 +++-
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index d0f81dad..1c021eee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -404,7 +404,8 @@ let rec canonize_name c =
 let build_subst uf subst =
   Array.map (fun i ->
 	       try term uf i
-	       with _ -> anomaly "incomplete matching") subst
+	       with e when Errors.noncritical e ->
+                 anomaly "incomplete matching") subst
 
 let rec inst_pattern subst = function
     PVar i ->
@@ -730,9 +731,7 @@ let __eps__ = id_of_string "_eps_"
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
   let {it=gl ; sigma=sigma} = state.gls in
-  let new_hyps =
-    Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in
-  let gls = Goal.V82.new_goal_with sigma gl new_hyps in
+  let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
     state.gls<- gls;
     id
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 95ff4d34..764e36b0 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -129,7 +129,9 @@ let non_trivial = function
 
 let patterns_of_constr env sigma nrels term=
   let f,args=
-    try destApp (whd_delta env term) with _ -> raise Not_found in
+    try destApp (whd_delta env term)
+    with e when Errors.noncritical e -> raise Not_found
+  in
 	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
-- 
cgit v1.2.3