From 07c5372510a5abecd788aa0b500e5deaa548c9d4 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 14 May 2007 16:37:18 +0000
Subject: [PATCH] CSC: terrific bug fixed. Enrico commented the application of
eta_fix to the body of a constant, without replacing it with Unshare.unshare
(that is done inside eta_fix). To avoid the bug to happear again, I have
renamed eta_fix in eta_fix_and_unshare.
---
helm/software/components/cic_acic/cic2acic.ml | 20 +++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index 89d3d00b4..bb00476b9 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -508,30 +508,30 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
let aconjecture_of_conjecture' = aconjecture_of_conjecture seed
ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
ids_to_hypotheses hypotheses_seed in
- let eta_fix metasenv context t =
+ let eta_fix_and_unshare metasenv context t =
let t = if eta_fix then E.eta_fix metasenv context t else t in
Unshare.unshare t in
let aobj =
match obj with
C.Constant (id,Some bo,ty,params,attrs) ->
- let bo' = (*eta_fix [] []*) bo in
- let ty' = eta_fix [] [] ty in
+ let bo' = (*eta_fix_and_unshare[] [] bo*) Unshare.unshare bo in
+ let ty' = eta_fix_and_unshare [] [] ty in
let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
C.AConstant
("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
| C.Constant (id,None,ty,params,attrs) ->
- let ty' = eta_fix [] [] ty in
+ let ty' = eta_fix_and_unshare [] [] ty in
let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
C.AConstant
("mettereaposto",None,id,None,aty,params,attrs)
| C.Variable (id,bo,ty,params,attrs) ->
- let ty' = eta_fix [] [] ty in
+ let ty' = eta_fix_and_unshare [] [] ty in
let abo =
match bo with
None -> None
| Some bo ->
- let bo' = eta_fix [] [] bo in
+ let bo' = eta_fix_and_unshare [] [] bo in
Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty'))
in
let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
@@ -548,16 +548,16 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
match d with
None -> None
| Some (n, C.Decl t)->
- Some (n, C.Decl (eta_fix conjectures canonical_context' t))
+ Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t))
| Some (n, C.Def (t,None)) ->
Some (n,
- C.Def ((eta_fix conjectures canonical_context' t),None))
+ C.Def ((eta_fix_and_unshare conjectures canonical_context' t),None))
| Some (_,C.Def (_,Some _)) -> assert false
in
d::canonical_context'
) canonical_context []
in
- let term' = eta_fix conjectures canonical_context' term in
+ let term' = eta_fix_and_unshare conjectures canonical_context' term in
(i,canonical_context',term')
) conjectures
in
@@ -573,7 +573,7 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
conjectures' in
(* let bo' = eta_fix conjectures' [] bo in *)
let bo' = bo in
- let ty' = eta_fix conjectures' [] ty in
+ let ty' = eta_fix_and_unshare conjectures' [] ty in
(*
let time2 = Sys.time () in
prerr_endline
--
2.39.5