exception Fail of string;;
+(*CSC: generatore di nomi? Chiedere il nome? *)
+let fresh_name =
+ let next_fresh_index = ref 0
+in
+ function () ->
+ incr next_fresh_index ;
+ "fresh_name" ^ string_of_int !next_fresh_index
+;;
+
(* lambda_abstract newmeta ty *)
(* returns a triple [bo],[context],[ty'] where *)
(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
match n with
C.Name _ -> n
(*CSC: generatore di nomi? Chiedere il nome? *)
- | C.Anonimous -> C.Name "fresh_name"
+ | C.Anonimous -> C.Name (fresh_name ())
in
((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
| C.LetIn (n,s,t) ->
metano,context,ty
in
let context = cic_context_of_named_context context in
- if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
+ if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then
begin
refine_meta metano bo [] ;
goal := None
None -> assert false
| Some (metano,(context,ty)) -> metano,context,ty
in
- let term' = reduction_function term in
+ let ciccontext = cic_context_of_named_context context in
+ let term' = reduction_function ciccontext term in
(* We don't know if [term] is a subterm of [ty] or a subterm of *)
(* the type of one metavariable. So we replace it everywhere. *)
(*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
None -> []
| Some (_,(context,_)) -> context
in
- let term' = reduction_function term in
+ let ciccontext = cic_context_of_named_context context in
+ let term' = reduction_function ciccontext term in
ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
;;
None -> assert false
| Some (metano,(context,ty)) -> metano,context,ty
in
- let term' = CicReduction.whd term in
+ let ciccontext = cic_context_of_named_context context in
+ let term' = CicReduction.whd ciccontext term in
(* We don't know if [term] is a subterm of [ty] or a subterm of *)
(* the type of one metavariable. So we replace it everywhere. *)
(*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
let ciccontext = cic_context_of_named_context context in
(* are_convertible works only on well-typed terms *)
ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
- if CicReduction.are_convertible goal_input input then
+ if CicReduction.are_convertible ciccontext goal_input input then
begin
let ty' = ProofEngineReduction.replace goal_input input ty in
let metasenv' =