| C.LetIn (_,s,t) -> (aux s) @ (aux t)
| C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
| C.Const _
| C.LetIn (_,s,t) -> (aux s) @ (aux t)
| C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
| C.Const _
| C.MutInd _
| C.MutConstruct _ -> []
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
| C.MutInd _
| C.MutConstruct _ -> []
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
| C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
| C.Appl l -> C.Appl (List.map (aux n) l)
| C.Const _ as t -> t
| C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
| C.Appl l -> C.Appl (List.map (aux n) l)
| C.Const _ as t -> t
| C.MutInd _
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
| C.MutInd _
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
(* the type of one metavariable. So we replace it everywhere. *)
(*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
(*CSC: che si guadagni nulla in fatto di efficienza. *)
(* the type of one metavariable. So we replace it everywhere. *)
(*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
(*CSC: che si guadagni nulla in fatto di efficienza. *)
- let replace = ProofEngineReduction.replace
- ~equality:(==) ~what:term' ~with_what:term
+ let replace =
+ ProofEngineReduction.replace
+ ~equality:(ProofEngineReduction.syntactic_equality)
+ ~what:term' ~with_what:term