The user interface for the completeSearchPattern query has been improved.

[helm.git] / helm / gTopLevel / proofEngineReduction.ml

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 0446132c5163a022c46d5314992768886d72d6e6..208864c801f1a2fdeafa99506ade65b46f901f51 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -42,6 +42,7 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 exception WrongUriToInductiveDefinition;;
+exception WrongUriToConstant;;
 exception RelToHiddenHypothesis;;
 
 let alpha_equivalence =
@@ -444,7 +445,7 @@ let reduce context =
         in
          if l = [] then t' else C.Appl (t'::l)
  and reduceaux_exp_named_subst context l =
-  List.map (function uri,t -> uri,reduceaux context l t)
+  List.map (function uri,t -> uri,reduceaux context [] t)
  in
   reduceaux context []
 ;;
@@ -475,7 +476,7 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 let simpl context =
  (* reduceaux is equal to the reduceaux locally defined inside *)
- (*reduce, but for the const case.                             *) 
+ (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
  let rec reduceaux context l =
   let module C = Cic in
@@ -583,13 +584,18 @@ let simpl context =
                  aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
                in
                 (**** Step 3 ****)
-                let term_to_fold =
-                 match constant_args with
-                    [] -> C.Const (uri,exp_named_subst')
-                  | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args)
+                let term_to_fold, delta_expanded_term_to_fold =
+                 let body' = CicSubstitution.subst_vars exp_named_subst' body in
+                  match constant_args with
+                     [] -> C.Const (uri,exp_named_subst'), body'
+                   | _ ->
+                     C.Appl ((C.Const (uri,exp_named_subst'))::constant_args),
+                      C.Appl (body'::constant_args)
                 in
-                 let reduced_term_to_fold = reduce context term_to_fold in
-                  replace (=) reduced_term_to_fold term_to_fold res
+                 let simplified_term_to_fold =
+                  reduceaux context [] delta_expanded_term_to_fold
+                 in
+                  replace (=) simplified_term_to_fold term_to_fold res
               with
                  WrongShape ->
                   (* The constant does not unfold to a Fix lambda-abstracted  *)
@@ -604,11 +610,8 @@ let simpl context =
                    if l = [] then t' else C.Appl (t'::l)
              end
          | C.Constant (_,None,_,_) ->
-            let exp_named_subst' =
-             reduceaux_exp_named_subst context l exp_named_subst
-            in
-             let t' = C.Const (uri,exp_named_subst') in
-              if l = [] then t' else C.Appl (t'::l)
+            let t' = C.Const (uri,exp_named_subst') in
+             if l = [] then t' else C.Appl (t'::l)
          | C.Variable _ -> raise ReferenceToVariable
          | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -739,7 +742,7 @@ let simpl context =
        in
          if l = [] then t' else C.Appl (t'::l)
  and reduceaux_exp_named_subst context l =
-  List.map (function uri,t -> uri,reduceaux context l t)
+  List.map (function uri,t -> uri,reduceaux context [] t)
  in
   reduceaux context []
 ;;