X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineHelpers.ml;h=74b6fcdaca1f344032da1afc7df9c393f30f9206;hb=81cc12ae4ebd9741585b38f41c7fb5eb6c5ae916;hp=7e5f3a4b19b6468f527f5c67702991dbbbe12962;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git

diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml
index 7e5f3a4b1..74b6fcdac 100644
--- a/helm/gTopLevel/proofEngineHelpers.ml
+++ b/helm/gTopLevel/proofEngineHelpers.ml
@@ -23,6 +23,17 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(*CSC: generatore di nomi? Chiedere il nome? *)
+let fresh_name =
+ let next_fresh_index = ref 0 in
+  function
+     Cic.Anonymous ->
+      incr next_fresh_index ;
+      "fresh_name" ^ string_of_int !next_fresh_index
+   | Cic.Name name ->
+      incr next_fresh_index ;
+      name ^ string_of_int !next_fresh_index
+
 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 (* where n = List.length [canonical_context]                             *)
@@ -40,11 +51,7 @@ let identity_relocation_list_for_metavariable canonical_context =
 (* Returns the first meta whose number is above the *)
 (* number of the higher meta.                       *)
 let new_meta ~proof =
- let metasenv =
-  match proof with
-     None -> assert false
-   | Some (_,metasenv,_,_) -> metasenv
- in
+ let (_,metasenv,_,_) = proof in
   let rec aux =
    function
       None,[] -> 1
@@ -55,11 +62,7 @@ let new_meta ~proof =
    1 + aux (None,metasenv)
 
 let subst_meta_in_proof proof meta term newmetasenv =
- let (uri,metasenv,bo,ty) =
-  match proof with
-     None -> assert false
-   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
- in
+ let uri,metasenv,bo,ty = proof in
   let subst_in = CicUnification.apply_subst [meta,term] in
    let metasenv' =
     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
@@ -79,7 +82,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
       ) metasenv'
     in
      let bo' = subst_in bo in
-      let newproof = Some (uri,metasenv'',bo',ty) in
+      let newproof = uri,metasenv'',bo',ty in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -95,11 +98,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
 (*CSC: [newmetasenv].                                             *)
 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,bo,ty) =
-  match proof with
-     None -> assert false
-   | Some (uri,_,bo,ty) -> uri,bo,ty
- in
+ let (uri,_,bo,ty) = proof in
   let bo' = subst_in bo in
   let metasenv' =
    List.fold_right
@@ -118,6 +117,6 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
        | _ -> i
     ) newmetasenv []
   in
-   let newproof = Some (uri,metasenv',bo',ty) in
+   let newproof = uri,metasenv',bo',ty in
     (newproof, metasenv')