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 9771b7d821d023e861144e34b71234739d9feb8f..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
@@ -246,10 +246,7 @@ let reduce =
        in
         if l = [] then t' else C.Appl (t'::l)
  in
-function t -> let res =
-prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
   reduceaux []
-t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
 ;;
 
 exception WrongShape;;
@@ -277,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 ****)
@@ -340,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' =
@@ -365,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