Experimental commit: definitions are now allowed in contexts. As a consequence,

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

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 58aaa04386329ef8e0de0283fa449e84bc0612d2..94e5b353de3534df42cba3016327de56abffdd6c 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -91,7 +91,7 @@ let replace ~what ~with_what ~where =
 
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
-let reduce =
+let reduce context =
  let rec reduceaux l =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -274,7 +274,7 @@ exception WhatShouldIDo;;
 (*     change in every iteration, i.e. to the actual arguments for the       *)
 (*     lambda-abstractions that precede the Fix.                             *)
 (*CSC: It does not perform simplification in a Case *)
-let simpl =
+let simpl context =
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (*reduce, but for the const case.                             *) 
  (**** Step 1 ****)
@@ -337,7 +337,7 @@ let simpl =
                       with
                        _ -> raise AlreadySimplified
                      in
-                      (match CicReduction.whd recparam with
+                      (match CicReduction.whd context recparam with
                           C.MutConstruct _
                         | C.Appl ((C.MutConstruct _)::_) ->
                            let body' =
@@ -362,7 +362,7 @@ let simpl =
                    [] -> C.Const (uri,cookingsno)
                  | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
                in
-                let reduced_term_to_fold = reduce term_to_fold in
+                let reduced_term_to_fold = reduce context term_to_fold in
 prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
 prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
                  replace reduced_term_to_fold term_to_fold res