X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=fc508f0c11a33b85df8795ab5c63e487b3214dcb;hb=ee242468b221c64b25c99b52110fe00380f4eebe;hp=7d223a4437b4d9fe232032315b9ec8c933a17a6a;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index 7d223a443..fc508f0c1 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -56,7 +56,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
          i,canonical_context',(subst_in ty)
       ) metasenv'
     in
-     let bo' = subst_in bo in
+     let bo' = lazy (subst_in (Lazy.force bo)) in
      (* Metavariables can appear also in the *statement* of the theorem
       * since the parser does not reject as statements terms with
       * metavariable therein *)
@@ -79,7 +79,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
  let (uri,_,initial_subst,bo,ty, attrs) = proof in
   let subst_in = CicMetaSubst.apply_subst subst in
-  let bo' = subst_in bo in
+  let bo' = lazy (subst_in (Lazy.force bo)) in
   (* Metavariables can appear also in the *statement* of the theorem
    * since the parser does not reject as statements terms with
    * metavariable therein *)
@@ -640,6 +640,32 @@ let lookup_type metasenv context hyp =
    in
    aux 1 context
 
+let find_hyp name =
+ let rec find_hyp n =
+  function
+     [] -> assert false
+   | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
+      Cic.Rel n, CicSubstitution.lift n ty
+   | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
+   | _::tl -> find_hyp (n+1) tl
+ in
+  find_hyp 1
+;;
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+let sort_pattern_hyps context (t,hpatterns,cpattern) =
+ let hpatterns =
+  List.sort
+   (fun (id1,_) (id2,_) ->
+     let t1,_ = find_hyp id1 context in
+     let t2,_ = find_hyp id2 context in
+     match t1,t2 with
+        Cic.Rel n1, Cic.Rel n2 -> compare n1 n2
+      | _,_ -> assert false) hpatterns
+ in
+  t,hpatterns,cpattern
+;;
+
 (* FG: **********************************************************************)
 
 let get_name context index =